How to prove uniqueness with uniqueness quantification? (Uniqueness of the Axiom of Specification)

Question

I really like the uniqueness quantifier $\exists!$, but I don't know how to prove formulae with it.

I am trying to prove: $$\forall X\exists!Y\forall x(x\in Y\iff x\in X\land\phi(x))$$

from the ZFC axiom schema of specification, $$\forall X\exists Y\forall x(x\in Y\iff x\in X\land\phi(x))$$

the ZFC axiom of extensionality: $$\forall X,Y(\forall x(x\in X\iff x\in Y)\implies X=Y)$$

and one of the following definitions of the uniqueness quantifier:
$\exists! x\phi(x)\dashv\vdash$ $$\exists x(\phi(x)\land\neg\exists y(\phi(y)\land x\neq y))$$ $$\text{OR}$$ $$\exists x(\phi(x)\land\forall y(\phi(y)\implies x=y))$$ $$\text{OR}$$ $$\exists x\forall y(\phi(y)\iff x=y)$$

Predicate Logic with Equality is assumed.

Here is my work:

1. $\exists Y\forall x(x\in Y\iff x\in X\land\phi(x))$ axiom of specification $X$/$X$
2. $\forall x(x\in Y_1\iff x\in X\land\phi(x))$ existential instantiation 1 $Y_1$/$Y$
3. $x\in Y_1\iff x\in X\land\phi(x)$ universal instantiation 2 $x$/$x$
4. $\forall x(x\in Y_2\iff x\in X\land\phi(x))$ existential instantiation 1 $Y_2$/$Y$
5. $x\in Y_2\iff x\in X\land\phi(x)$ universal instantiation 4 $x$/$x$
6. $x\in X\land\phi(x)\iff x\in Y_2$ commutativity of equivalence 5
7. $(x\in Y_1\iff x\in X\land\phi(x))\land (x\in X\land\phi(x)\iff x\in Y_2)$ adjunction 3,6
8. $((x\in Y_1\iff x\in X\land\phi(x))\land (x\in X\land\phi(x)\iff x\in Y_2))\implies (x\in Y_1\iff x\in Y_2)$ logical truth
9. $x\in Y_1\iff x\in Y_2$ modus ponendo ponens 8,7
10. $\forall x(x\in Y_1\iff x\in Y_2)$ universal generalization 9 $x$/$x$
11. $\forall x(x\in Y_1\iff x\in Y_2)\implies Y_1=Y_2$ axiom of extensionality $Y_1$/$X$, $Y_2$/$Y$
12. $Y_1=Y_2$ modus ponendo ponens 11,10

How should one finish the proof?

(This is not for school)

Answer 1

The approach is correct.

You have 2) $∀x(x∈Y_1 ⟺ x∈X ∧ ϕ(x))$; call it $\psi(Y_1)$.

Now assume 2') $\psi(Z)$ and $Z \ne Y_1$.

From $\psi(Z)$, i.e $∀x(x∈Z ⟺ x∈X ∧ ϕ(x))$, we have $x∈Z ⟺ x∈X ∧ ϕ(x)$ and thus, with 3) above: $x∈Z ⟺ x∈Y_1$, from which, by Extensionality: $Z=Y_1$.

This contradicts $Z \ne Y_1$ and thus we conclude with $Z = Y_1$ by Double Negation.

Now we discharge assumption 2') to get $\psi(Z) \to Z=Y_1$.

Variable $Z$ is not free in any assumption, thus we can use Generalization to get: $\forall Z [∀x(x∈Z ⟺ x∈X ∧ ϕ(x)) \to Z=Y_1]$.

With 2) we get:

$∀x(x∈Y_1 ⟺ x∈X ∧ ϕ(x)) \land \forall Z [∀x(x∈Z ⟺ x∈X ∧ ϕ(x)) \to Z=Y_1]$

and by Existential introduction: $\exists Y \forall x(x∈Y ⟺ x∈X ∧ ϕ(x)) \land \forall Z [∀x(x∈Z ⟺ x∈X ∧ ϕ(x)) \to Z=Y]$.

The last formula is:

$\exists !Y \forall x(x∈Y ⟺ x∈X ∧ ϕ(x))$.