Proof of Theorem 2sb5rf
Step | Hyp | Ref
| Expression |
1 | | 2sb5rf.1 |
. . 3
⊢ (φ → ∀zφ) |
2 | 1 | sb5rf 1729 |
. 2
⊢ (φ ↔ ∃z(z = x ∧ [z / x]φ)) |
3 | | 19.42v 1783 |
. . . 4
⊢ (∃w(z = x ∧ (w = y ∧ [w / y][z / x]φ)) ↔ (z = x ∧ ∃w(w = y ∧ [w / y][z / x]φ))) |
4 | | sbcom2 1860 |
. . . . . . 7
⊢
([z / x][w / y]φ ↔
[w / y][z / x]φ) |
5 | 4 | anbi2i 430 |
. . . . . 6
⊢
(((z = x ∧ w = y) ∧ [z / x][w / y]φ) ↔
((z = x
∧ w =
y) ∧
[w / y][z / x]φ)) |
6 | | anass 381 |
. . . . . 6
⊢
(((z = x ∧ w = y) ∧ [w / y][z / x]φ) ↔
(z = x
∧ (w =
y ∧
[w / y][z / x]φ))) |
7 | 5, 6 | bitri 173 |
. . . . 5
⊢
(((z = x ∧ w = y) ∧ [z / x][w / y]φ) ↔
(z = x
∧ (w =
y ∧
[w / y][z / x]φ))) |
8 | 7 | exbii 1493 |
. . . 4
⊢ (∃w((z = x ∧ w = y) ∧ [z / x][w / y]φ) ↔ ∃w(z = x ∧ (w = y ∧ [w / y][z / x]φ))) |
9 | | 2sb5rf.2 |
. . . . . . 7
⊢ (φ → ∀wφ) |
10 | 9 | hbsbv 1814 |
. . . . . 6
⊢
([z / x]φ →
∀w[z / x]φ) |
11 | 10 | sb5rf 1729 |
. . . . 5
⊢
([z / x]φ ↔
∃w(w = y ∧ [w / y][z / x]φ)) |
12 | 11 | anbi2i 430 |
. . . 4
⊢
((z = x ∧ [z / x]φ) ↔ (z = x ∧ ∃w(w = y ∧ [w / y][z / x]φ))) |
13 | 3, 8, 12 | 3bitr4ri 202 |
. . 3
⊢
((z = x ∧ [z / x]φ) ↔ ∃w((z = x ∧ w = y) ∧ [z / x][w / y]φ)) |
14 | 13 | exbii 1493 |
. 2
⊢ (∃z(z = x ∧ [z / x]φ) ↔
∃z∃w((z = x ∧ w = y) ∧ [z / x][w / y]φ)) |
15 | 2, 14 | bitri 173 |
1
⊢ (φ ↔ ∃z∃w((z = x ∧ w = y) ∧ [z / x][w / y]φ)) |