Proof of Theorem sbcof2
Step | Hyp | Ref
| Expression |
1 | | sbcof2.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥𝜑) |
2 | 1 | hbsb3 1801 |
. . . . . 6
⊢ ([𝑥 / 𝑦]𝜑 → ∀𝑦[𝑥 / 𝑦]𝜑) |
3 | 2 | sb6f 1796 |
. . . . 5
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) |
4 | 1 | sb6f 1796 |
. . . . . . 7
⊢ ([𝑥 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → 𝜑)) |
5 | 4 | imbi2i 225 |
. . . . . 6
⊢ ((𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
6 | 5 | albii 1463 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
7 | 3, 6 | bitri 183 |
. . . 4
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑))) |
8 | | ax-11 1499 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)))) |
9 | | equcomi 1697 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
10 | 9 | imim1i 60 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑥 → 𝜑) → (𝑥 = 𝑦 → 𝜑)) |
11 | 10 | imim2i 12 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑))) |
12 | 11 | pm2.43d 50 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → 𝜑)) |
13 | 12 | alimi 1448 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
14 | 8, 13 | syl6 33 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
15 | 14 | a2i 11 |
. . . . 5
⊢ ((𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
16 | 15 | alimi 1448 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
17 | 7, 16 | sylbi 120 |
. . 3
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
18 | | ax-i9 1523 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
19 | | exim 1592 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))) |
20 | 18, 19 | mpi 15 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)) |
21 | | ax-ial 1527 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)) |
22 | 21 | 19.9h 1636 |
. . . 4
⊢
(∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
23 | 20, 22 | sylib 121 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
24 | | sb2 1760 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) |
25 | 17, 23, 24 | 3syl 17 |
. 2
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → [𝑦 / 𝑥]𝜑) |
26 | | sb1 1759 |
. . . 4
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
27 | | simpl 108 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦) |
28 | | 19.8a 1583 |
. . . . . 6
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
29 | 27, 28 | jca 304 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
30 | 29 | eximi 1593 |
. . . 4
⊢
(∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
31 | 9 | anim1i 338 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑦 = 𝑥 ∧ 𝜑)) |
32 | 27, 31 | jca 304 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑))) |
33 | 32 | eximi 1593 |
. . . . . . 7
⊢
(∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑))) |
34 | | ax11e 1789 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
35 | 33, 34 | syl5 32 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
36 | 35 | imdistani 443 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
37 | 36 | eximi 1593 |
. . . 4
⊢
(∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
38 | 26, 30, 37 | 3syl 17 |
. . 3
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
39 | 2 | sb5f 1797 |
. . . 4
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) |
40 | 1 | sb5f 1797 |
. . . . . 6
⊢ ([𝑥 / 𝑦]𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)) |
41 | 40 | anbi2i 454 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
42 | 41 | exbii 1598 |
. . . 4
⊢
(∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
43 | 39, 42 | bitri 183 |
. . 3
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))) |
44 | 38, 43 | sylibr 133 |
. 2
⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥][𝑥 / 𝑦]𝜑) |
45 | 25, 44 | impbii 125 |
1
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) |