ZFC: axiomatic set theory

Which axiom is used to show that for any sets $a$ and $b$ the intersection $a \cap b = \{z \in a \mid z \in b\}$ is a set?

The stages of the cumulative hierarchy are $V_0 = \varnothing$ and $V_{n+1} = \mathcal P(V_n)$. We know $|V_4| = 16$. How many elements does $V_5$ have?

How many elements does the Kuratowski pair $(a, a) = \{\{a\}, \{a, a\}\}$ have?

In the proof that there is no set $U$ containing every set, we form $R = \{x \in U \mid x \notin x\}$. Which axiom guarantees that $R$ is a set?

Which of these proposed definitions of an ordered pair fail the requirement that $\langle a, b \rangle = \langle c, d \rangle$ implies $a = c$ and $b = d$? Select all that fail.

Assume ZFC is consistent. Which of these statements does ZFC not prove? Select all.

Zermelo's system ZC is ZFC without Replacement (and without Foundation). The stage $V_{\omega + \omega}$ is a model of ZC. Which set's existence can therefore not be proved in ZC?

Which Lean statement formalises “no set is a member of itself” for Mathlib's model ZFSet?

Represent sets by Python frozensets. Write numeral(n) (von Neumann: 0 is the empty frozenset and n + 1 = n ∪ {n}), kpair(a, b) returning the Kuratowski pair $\{\{a\}, \{a, b\}\}$, and first(p) and second(p) that recover $a$ and $b$ from such a pair. Hint: $a$ belongs to every element of $p$; $b$ is the element of $\bigcup p$ that is not $a$ — unless $\bigcup p = \{a\}$.