Proof of Theorem mor
Step | Hyp | Ref
| Expression |
1 | | mor.1 |
. . 3
⊢
Ⅎyφ |
2 | 1 | sb8e 1734 |
. 2
⊢ (∃xφ ↔ ∃y[y / x]φ) |
3 | | impexp 250 |
. . . . 5
⊢ (((φ ∧
[y / x]φ) →
x = y)
↔ (φ → ([y / x]φ → x = y))) |
4 | | bi2.04 237 |
. . . . 5
⊢ ((φ → ([y / x]φ → x = y)) ↔
([y / x]φ →
(φ → x = y))) |
5 | 3, 4 | bitri 173 |
. . . 4
⊢ (((φ ∧
[y / x]φ) →
x = y)
↔ ([y / x]φ →
(φ → x = y))) |
6 | 5 | 2albii 1357 |
. . 3
⊢ (∀x∀y((φ ∧
[y / x]φ) →
x = y)
↔ ∀x∀y([y / x]φ →
(φ → x = y))) |
7 | | nfs1v 1812 |
. . . . . 6
⊢
Ⅎx[y / x]φ |
8 | 7 | nfri 1409 |
. . . . 5
⊢
([y / x]φ →
∀x[y / x]φ) |
9 | 8 | eximi 1488 |
. . . 4
⊢ (∃y[y / x]φ → ∃y∀x[y / x]φ) |
10 | | alim 1343 |
. . . . . . 7
⊢ (∀x([y / x]φ → (φ → x = y)) →
(∀x[y / x]φ →
∀x(φ →
x = y))) |
11 | 10 | alimi 1341 |
. . . . . 6
⊢ (∀y∀x([y / x]φ → (φ → x = y)) →
∀y(∀x[y / x]φ →
∀x(φ →
x = y))) |
12 | 11 | a7s 1340 |
. . . . 5
⊢ (∀x∀y([y / x]φ → (φ → x = y)) →
∀y(∀x[y / x]φ →
∀x(φ →
x = y))) |
13 | | exim 1487 |
. . . . 5
⊢ (∀y(∀x[y / x]φ → ∀x(φ → x = y)) →
(∃y∀x[y / x]φ → ∃y∀x(φ → x = y))) |
14 | 12, 13 | syl 14 |
. . . 4
⊢ (∀x∀y([y / x]φ → (φ → x = y)) →
(∃y∀x[y / x]φ → ∃y∀x(φ → x = y))) |
15 | 9, 14 | syl5com 26 |
. . 3
⊢ (∃y[y / x]φ → (∀x∀y([y / x]φ → (φ → x = y)) →
∃y∀x(φ → x = y))) |
16 | 6, 15 | syl5bi 141 |
. 2
⊢ (∃y[y / x]φ → (∀x∀y((φ ∧
[y / x]φ) →
x = y)
→ ∃y∀x(φ →
x = y))) |
17 | 2, 16 | sylbi 114 |
1
⊢ (∃xφ → (∀x∀y((φ ∧
[y / x]φ) →
x = y)
→ ∃y∀x(φ →
x = y))) |