Proof using predicate logic to show subsets from axiom schema of specification are unique I would like to prove that axiom of specification and axiom of extensionality implies that set constructed from axiom of specification is unique.  I understand the arguments given by words but I would like to practice and prove it using predicate logic and inference rules. 
I would be happy if you could help or hint me about how to prove a specific part that I am stuck with. I will show you my reasoning below. I would also appreciate if there would be some comments on how to make proof easier or more readable.
I want to show that for all formula $\phi$ assumptions $\forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ and $\forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ prove that $\forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$.
My sketch of the proof proceeds as follows.
$1. \forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$    (premise)
$2. \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 1)
$3. \exists y : \forall z: (z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 2)
$4. \forall z: (z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $b$)
$5. \forall z: (z \in c \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $c$)
$6. d \in b \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 4)
$7. d \in c \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 5)
$8. d \in c \iff d \in b$ (modus ponens on 6 and 7 using the following tautology: $(p \iff q) \land (q \iff r) \to (p \iff r)$)
$9. \forall z: (z \in c \iff z \in b)$ (universal generalization from 8 because $d$ was arbitrary)
$10. \forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ (premise)
$11. \forall y: (c = y \iff (\forall z:(z \in c \iff z \in y)))$ (universal instantiation from 10)
$12. c = b \iff (\forall z: (z \in c \iff z \in b))$ (universal instantiation from 11)
$13. c = b$ (modus ponens from 9 and 12 using the following tautology: $p \land (p \iff q) \to q$)
Here is the point I get stuck because I would like to prove for uniqueness that $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z)) \to r = b$ but from step 13 I (at least I think so) can prove only existence because $b$ and $c$ were not arbitrary but specifically chosen (kind of).
Let us assume that I have proven $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b)$ as step 100.
$101. \forall z:(z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b))$ 
(modus ponens from 4 and 100)
$102. \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$ 
(existential generalization of 101)
$103. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \iff \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$  
(tautology due to the definition of "exists unique")
$104. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (modus ponens from 103 and 104 using the following tautology: $p \land (p \iff q) \to q$)
$105. \forall x: \exists! y: \forall z:(z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 104 due to the fact that $a$ was arbitrary)
$106. \forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 105 due to the variables $w_1, ..., w_n$ being arbitrary)
This completes the proof. Any suggestions are very welcomed.
 A: An attempt to re-structure the proof...

*

*$∀x ∃y ∀z (z∈y⟺(z∈x ∧ ϕ(z)))$ --- axiom

2.-3. $∃y ∀z (z∈y⟺(z∈a ∧ ϕ(z)))$ --- universal instantiation from 1


*$∀z (z∈b⟺(z∈a ∧ ϕ(z)))$ --- existential instantiation from 3, for some $b$
4a. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- new premise


*$∀z(z∈c⟺(z∈a∧ϕ(z))) ∧ d≠b$ --- existential instantiation from 4a, for some $c$
5a  $∀z(z∈c⟺(z∈a∧ϕ(z)))$ --- from 5. by taut: $(p \land q) \to p$ and mp
5b. $c≠b$ --- from 5. by taut: $(p \land q) \to q$ and mp
5c. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to \lnot (c=b)$ --- from 5b by taut: $p \to (q \to p)$ and mp


*$d∈b⟺(d∈a ∧ ϕ(d))$ --- from 4


*$d∈c⟺(d∈a ∧ ϕ(d))$ --- from 5


*$d∈c ⟺ d∈b$ --- from 6 and 7


*$∀z (z∈c⟺z∈b)$ --- from 8 by universal generalization


*$c=b$ --- from 9 by extensionality


*$∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to (c=b)$ --- from 4a and 10 by Deduction Th, discharging premises 4a



*$\lnot ∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- from 5c and 11 and taut: $(p \to \lnot q) \to [(p \to q) \to \lnot p]$ (ex falso)




*$∀y[∀z(z∈y⟺(z∈a∧ϕ(z))) \to y=b]$ --- from 12 by equivalence for quantifiers and taut: $\lnot (p \land \lnot q) \Leftrightarrow (p \to q)$


