Proof of Theorem sbel2x
Step | Hyp | Ref
| Expression |
1 | | sbelx 1870 |
. . . . 5
⊢
([x / z]φ ↔
∃y(y = w ∧ [y / w][x / z]φ)) |
2 | 1 | anbi2i 430 |
. . . 4
⊢
((x = z ∧ [x / z]φ) ↔ (x = z ∧ ∃y(y = w ∧ [y / w][x / z]φ))) |
3 | 2 | exbii 1493 |
. . 3
⊢ (∃x(x = z ∧ [x / z]φ) ↔
∃x(x = z ∧ ∃y(y = w ∧ [y / w][x / z]φ))) |
4 | | sbelx 1870 |
. . 3
⊢ (φ ↔ ∃x(x = z ∧ [x / z]φ)) |
5 | | exdistr 1784 |
. . 3
⊢ (∃x∃y(x = z ∧ (y = w ∧ [y / w][x / z]φ)) ↔ ∃x(x = z ∧ ∃y(y = w ∧ [y / w][x / z]φ))) |
6 | 3, 4, 5 | 3bitr4i 201 |
. 2
⊢ (φ ↔ ∃x∃y(x = z ∧ (y = w ∧ [y / w][x / z]φ))) |
7 | | anass 381 |
. . 3
⊢
(((x = z ∧ y = w) ∧ [y / w][x / z]φ) ↔
(x = z
∧ (y =
w ∧
[y / w][x / z]φ))) |
8 | 7 | 2exbii 1494 |
. 2
⊢ (∃x∃y((x = z ∧ y = w) ∧ [y / w][x / z]φ) ↔ ∃x∃y(x = z ∧ (y = w ∧ [y / w][x / z]φ))) |
9 | 6, 8 | bitr4i 176 |
1
⊢ (φ ↔ ∃x∃y((x = z ∧ y = w) ∧ [y / w][x / z]φ)) |