Proof of Theorem sbccomlem
Step | Hyp | Ref
| Expression |
1 | | excom 2166 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑦∃𝑥(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑))) |
2 | | exdistr 1962 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝜑))) |
3 | | an12 642 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ (𝑦 = 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑))) |
4 | 3 | exbii 1854 |
. . . . . 6
⊢
(∃𝑥(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑦 = 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑))) |
5 | | 19.42v 1961 |
. . . . . 6
⊢
(∃𝑥(𝑦 = 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜑)) ↔ (𝑦 = 𝐵 ∧ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
6 | 4, 5 | bitri 274 |
. . . . 5
⊢
(∃𝑥(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ (𝑦 = 𝐵 ∧ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
7 | 6 | exbii 1854 |
. . . 4
⊢
(∃𝑦∃𝑥(𝑥 = 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
8 | 1, 2, 7 | 3bitr3i 301 |
. . 3
⊢
(∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝜑)) ↔ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
9 | | sbc5 3748 |
. . 3
⊢
([𝐴 / 𝑥]∃𝑦(𝑦 = 𝐵 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝜑))) |
10 | | sbc5 3748 |
. . 3
⊢
([𝐵 / 𝑦]∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) |
11 | 8, 9, 10 | 3bitr4i 303 |
. 2
⊢
([𝐴 / 𝑥]∃𝑦(𝑦 = 𝐵 ∧ 𝜑) ↔ [𝐵 / 𝑦]∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
12 | | sbc5 3748 |
. . 3
⊢
([𝐵 / 𝑦]𝜑 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝜑)) |
13 | 12 | sbcbii 3781 |
. 2
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐴 / 𝑥]∃𝑦(𝑦 = 𝐵 ∧ 𝜑)) |
14 | | sbc5 3748 |
. . 3
⊢
([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
15 | 14 | sbcbii 3781 |
. 2
⊢
([𝐵 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
16 | 11, 13, 15 | 3bitr4i 303 |
1
⊢
([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |