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.

• Regarding readibility, you can omit $w_1, \ldots, w_n$; they are needed for "generailty" but add nothing to the proof. – Mauro ALLEGRANZA Mar 18 '18 at 13:01
• In steps 6 and 7 you have to replace also the rightmost $z$ with $d$. – Mauro ALLEGRANZA Mar 18 '18 at 13:03
• Probably, the startegy must be: let $c$ be such that $∀z (z∈c ⟺ (z∈a ∧ ϕ(z)))$. Now assume that $\exists y [∀z (z∈y ⟺ (z∈a ∧ ϕ(z))) \land y \ne c]$. – Mauro ALLEGRANZA Mar 18 '18 at 13:14
• Let $c$... you have it already in 5. Tt is the "gist" of existential instantiation: having proved that $\exists x Px$ we call it $c$ and we have $Pc$. – Mauro ALLEGRANZA Mar 18 '18 at 15:23
• You can see e.g. Mendelson, page 34. – Mauro ALLEGRANZA Mar 18 '18 at 15:46

An attempt to re-structure the proof...

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

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

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

1. $∀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

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

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

3. $d∈c ⟺ d∈b$ --- from 6 and 7

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

5. $c=b$ --- from 9 by extensionality

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

1. $\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)
1. $∀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)$
• Thanks! It really helped! – Daniels Krimans Mar 19 '18 at 19:24