How to prove axiom of pairs from power set axiom and replacement?

This the exercise 2 of section 6 of chapter 1 of "Set Theory: An Introduction to Large Cardinals", by Frank R. Drake:

Show that A4 can be deduced from A3, and that A3 can be deduced from A9. Show that $\mathcal{P}(\mathcal{P}(\emptyset))$ has just two members, and hence that A5 can be deduced from A6 and A9.

The axioms are:

A1) Extensionality: $\forall z:(z\in x\Leftrightarrow z\in y)\Rightarrow x=y$

A2) Foundation: $\exists y:y\in x\Rightarrow\exists y:(y\in x \wedge \forall z:\neg(z\in x\wedge z\in y))$

A3) Separation: $\exists y:\forall x:(x\in y\Leftrightarrow (x\in a\wedge \varphi(x)\;))$

A4) Empty set: $\exists y:\forall x:\neg x\in y$

A5) Pairs: $\exists y:\forall x:(x\in y\Leftrightarrow x=a\vee x=b)$

A6) Power set: $\exists y:\forall x:(x\in y\Leftrightarrow \forall z:(z\in x\Rightarrow z\in a))$

A7) Union: $\exists y:\forall x:(x\in y\Leftrightarrow\exists z:(x\in z\wedge z\in a))$

A8) Infinity: $\exists w:(\exists y:(y\in w\wedge\forall x:\neg x\in y)\wedge\forall x:(x\in w\Rightarrow\exists z:(z\in w\wedge\forall u:(u\in z\Leftrightarrow u\in x\vee u=x))))$

A9) Replacement: $\forall x,y,z:(\psi(x,y)\wedge\psi(x,z)\Rightarrow y=z)\Rightarrow \exists b:\forall y:(y\in b\Leftrightarrow\exists x:(x\in a\wedge\psi(x,y)))$

A10) Choice: $\forall x:(x\in z\Rightarrow(\exists y:y\in x\wedge\forall y:(y\in z\Rightarrow x=y\vee \forall z:\neg(z\in x\wedge z\in y)))\Rightarrow \exists u:\forall x:(x\in z\Rightarrow\exists v:\forall y:(y\in z\wedge y\in x\Leftrightarrow y=v))$

Can somebody verify if my following solution is correct?

If A3, then there exists a set $a$ (because we assume there is something), and being $\varphi(x)$ the formula $x\neq x$, there is a set $y$ such that $\forall x:(x\in y\Leftrightarrow (x\in a\wedge x\neq x))$, so $\forall x:x\notin y$, therefore A4.

If A9, then for every formula $\varphi(x)$ with appropriate conditions, if $\psi(x,y)$ is the formula $x=y\wedge\varphi(y)$, then $\forall x,y,z:(\psi(x,y)\wedge\psi(x,z)\Rightarrow y=z)$, so there is a set $b$ such that $\forall y:(y\in b\Leftrightarrow\exists x:(x\in a\wedge\psi(x,y)))$, so $\forall y:(y\in b\Leftrightarrow\exists x:(x\in a\wedge x=y\wedge \varphi(y))$, so $\forall y:(y\in b\Leftrightarrow y\in a\wedge \varphi(y))$, therefore A3.

If A6 and A9, then A3 and A4, so there a set $e$ such that $\forall x:x\notin e$, and by A6 there is a set $p$ such that $\forall x:(x\in p\Leftrightarrow \forall z:(z\in x\Rightarrow z\in e))$, but $\forall z:(z\in e\Rightarrow z\in e)$, so $e\in p$, but $e\notin e$, so $e\neq p$, and again by A6 there is a set $q$ such that $\forall x:(x\in q\Leftrightarrow \forall z:(z\in x\Rightarrow z\in p))$, but $\forall z:z\notin e$, so $\forall z:(z\in e\Rightarrow z\in p)$, and $\forall z:(z\in p\Rightarrow z\in p)$, so that $e\in q$ and $p\in q$, so by A3 there is a set $a$ such that $\forall x:(x\in a\Leftrightarrow x\in q\wedge(x=e\vee x=p))$, so $\forall x:(x\in a\Leftrightarrow x=e\vee x=p)$ (the set $\mathcal{P}(\mathcal{P}(\emptyset))$ may be thought as the $a$), therefore, for any two sets $u$ and $v$, being $\psi(x,y)$ the formula $(x=e\wedge y=u)\vee(x=p\wedge y=v)$, then $\forall x,y,z:(\psi(x,y)\wedge\psi(x,z)\Rightarrow y=z)$, so there is a set $b$ such that $\forall y:(y\in b\Leftrightarrow\exists x:(x\in a\wedge\psi(x,y)))$, so $\forall y:(y\in b\Leftrightarrow\exists x:(x\in a\wedge((x=e\wedge y=u)\vee(x=p\wedge y=v))))$, so $\forall y:(y\in b\Leftrightarrow\exists x:((x=e\wedge y=u)\vee(x=p\wedge y=v)))$, so $\forall y:(y\in b\Leftrightarrow y=u\vee y=v)$; therefore A5.

• In K.Kunen's text on Set Theory, there is another axiom; A0) Existence : $\;\exists x\;(x=x).$ In order to develop as much of the theory as possible, that does not assume Infinity, we need,as you say, to assume A0, as all the other axioms begin with "$\forall$". – DanielWainfleet Jun 24 '18 at 5:39
• My edit was merely extra brackets in A3)...( to remove ambiguity) and some extra space ( type \; inside the dollar-signs).... BTW you can use \iff for $\iff$. – DanielWainfleet Jun 24 '18 at 5:47

The final part is not correct - but not by your fault: The claim itself is false. We do need A1 at some place. Indeed, all we know about $p:=\mathcal P(\emptyset)$ is that its elements are precisely those sets $x$ with $\forall z\colon(z\in x\Rightarrow z\in \emptyset)$, which simplifies to $\forall z\colon z\notin x$, in other words, $x$ is empty. But without A1, we cannot exclude that there are two (or more) empty sets. With two empty sets $\emptyset$ and $\emptyset'$, the$^1$ set $\mathcal P(\mathcal P(\emptyset))$ has at leat $\emptyset$, $\emptyset'$, $\{\emptyset\}$, $\{\emptyset'\}$, and $\{\emptyset,\emptyset'\}$ as elements.
$^1$ In the absence of A1, we cannot even speak of "the" power set (or other set defined by any of the axioms) any more, in much the same way as we normally cannot speak of "the" infinite set or "the" choice function.