Proof of Theorem sbcof2
Step | Hyp | Ref
| Expression |
1 | | sbcof2.1 |
. . . . . . 7
⊢ (φ → ∀xφ) |
2 | 1 | hbsb3 1686 |
. . . . . 6
⊢
([x / y]φ →
∀y[x / y]φ) |
3 | 2 | sb6f 1681 |
. . . . 5
⊢
([y / x][x / y]φ ↔
∀x(x = y → [x /
y]φ)) |
4 | 1 | sb6f 1681 |
. . . . . . 7
⊢
([x / y]φ ↔
∀y(y = x → φ)) |
5 | 4 | imbi2i 215 |
. . . . . 6
⊢
((x = y → [x /
y]φ) ↔ (x = y →
∀y(y = x → φ))) |
6 | 5 | albii 1356 |
. . . . 5
⊢ (∀x(x = y →
[x / y]φ) ↔
∀x(x = y → ∀y(y = x →
φ))) |
7 | 3, 6 | bitri 173 |
. . . 4
⊢
([y / x][x / y]φ ↔
∀x(x = y → ∀y(y = x →
φ))) |
8 | | ax-11 1394 |
. . . . . . 7
⊢ (x = y →
(∀y(y = x → φ)
→ ∀x(x = y → (y =
x → φ)))) |
9 | | equcomi 1589 |
. . . . . . . . . . 11
⊢ (x = y →
y = x) |
10 | 9 | imim1i 54 |
. . . . . . . . . 10
⊢
((y = x → φ)
→ (x = y → φ)) |
11 | 10 | imim2i 12 |
. . . . . . . . 9
⊢
((x = y → (y =
x → φ)) → (x = y →
(x = y
→ φ))) |
12 | 11 | pm2.43d 44 |
. . . . . . . 8
⊢
((x = y → (y =
x → φ)) → (x = y →
φ)) |
13 | 12 | alimi 1341 |
. . . . . . 7
⊢ (∀x(x = y →
(y = x
→ φ)) → ∀x(x = y →
φ)) |
14 | 8, 13 | syl6 29 |
. . . . . 6
⊢ (x = y →
(∀y(y = x → φ)
→ ∀x(x = y → φ))) |
15 | 14 | a2i 11 |
. . . . 5
⊢
((x = y → ∀y(y = x →
φ)) → (x = y →
∀x(x = y → φ))) |
16 | 15 | alimi 1341 |
. . . 4
⊢ (∀x(x = y →
∀y(y = x → φ))
→ ∀x(x = y → ∀x(x = y →
φ))) |
17 | 7, 16 | sylbi 114 |
. . 3
⊢
([y / x][x / y]φ →
∀x(x = y → ∀x(x = y →
φ))) |
18 | | ax-i9 1420 |
. . . . 5
⊢ ∃x x = y |
19 | | exim 1487 |
. . . . 5
⊢ (∀x(x = y →
∀x(x = y → φ))
→ (∃x x = y → ∃x∀x(x = y →
φ))) |
20 | 18, 19 | mpi 15 |
. . . 4
⊢ (∀x(x = y →
∀x(x = y → φ))
→ ∃x∀x(x = y → φ)) |
21 | | ax-ial 1424 |
. . . . 5
⊢ (∀x(x = y →
φ) → ∀x∀x(x = y →
φ)) |
22 | 21 | 19.9h 1531 |
. . . 4
⊢ (∃x∀x(x = y →
φ) ↔ ∀x(x = y →
φ)) |
23 | 20, 22 | sylib 127 |
. . 3
⊢ (∀x(x = y →
∀x(x = y → φ))
→ ∀x(x = y → φ)) |
24 | | sb2 1647 |
. . 3
⊢ (∀x(x = y →
φ) → [y / x]φ) |
25 | 17, 23, 24 | 3syl 17 |
. 2
⊢
([y / x][x / y]φ →
[y / x]φ) |
26 | | sb1 1646 |
. . . 4
⊢
([y / x]φ →
∃x(x = y ∧ φ)) |
27 | | simpl 102 |
. . . . . 6
⊢
((x = y ∧ φ) → x = y) |
28 | | 19.8a 1479 |
. . . . . 6
⊢
((x = y ∧ φ) → ∃x(x = y ∧ φ)) |
29 | 27, 28 | jca 290 |
. . . . 5
⊢
((x = y ∧ φ) → (x = y ∧ ∃x(x = y ∧ φ))) |
30 | 29 | eximi 1488 |
. . . 4
⊢ (∃x(x = y ∧ φ) →
∃x(x = y ∧ ∃x(x = y ∧ φ))) |
31 | 9 | anim1i 323 |
. . . . . . . . 9
⊢
((x = y ∧ φ) → (y = x ∧ φ)) |
32 | 27, 31 | jca 290 |
. . . . . . . 8
⊢
((x = y ∧ φ) → (x = y ∧ (y = x ∧ φ))) |
33 | 32 | eximi 1488 |
. . . . . . 7
⊢ (∃x(x = y ∧ φ) →
∃x(x = y ∧ (y = x ∧ φ))) |
34 | | ax11e 1674 |
. . . . . . 7
⊢ (x = y →
(∃x(x = y ∧ (y = x ∧ φ)) →
∃y(y = x ∧ φ))) |
35 | 33, 34 | syl5 28 |
. . . . . 6
⊢ (x = y →
(∃x(x = y ∧ φ) → ∃y(y = x ∧ φ))) |
36 | 35 | imdistani 419 |
. . . . 5
⊢
((x = y ∧ ∃x(x = y ∧ φ)) →
(x = y
∧ ∃y(y = x ∧ φ))) |
37 | 36 | eximi 1488 |
. . . 4
⊢ (∃x(x = y ∧ ∃x(x = y ∧ φ)) → ∃x(x = y ∧ ∃y(y = x ∧ φ))) |
38 | 26, 30, 37 | 3syl 17 |
. . 3
⊢
([y / x]φ →
∃x(x = y ∧ ∃y(y = x ∧ φ))) |
39 | 2 | sb5f 1682 |
. . . 4
⊢
([y / x][x / y]φ ↔
∃x(x = y ∧ [x / y]φ)) |
40 | 1 | sb5f 1682 |
. . . . . 6
⊢
([x / y]φ ↔
∃y(y = x ∧ φ)) |
41 | 40 | anbi2i 430 |
. . . . 5
⊢
((x = y ∧ [x / y]φ) ↔ (x = y ∧ ∃y(y = x ∧ φ))) |
42 | 41 | exbii 1493 |
. . . 4
⊢ (∃x(x = y ∧ [x / y]φ) ↔
∃x(x = y ∧ ∃y(y = x ∧ φ))) |
43 | 39, 42 | bitri 173 |
. . 3
⊢
([y / x][x / y]φ ↔
∃x(x = y ∧ ∃y(y = x ∧ φ))) |
44 | 38, 43 | sylibr 137 |
. 2
⊢
([y / x]φ →
[y / x][x / y]φ) |
45 | 25, 44 | impbii 117 |
1
⊢
([y / x][x / y]φ ↔
[y / x]φ) |