Proof of Theorem gencbvex
Step | Hyp | Ref
| Expression |
1 | | excom 2168 |
. 2
⊢
(∃𝑥∃𝑦(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ ∃𝑦∃𝑥(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓))) |
2 | | gencbvex.1 |
. . . 4
⊢ 𝐴 ∈ V |
3 | | gencbvex.3 |
. . . . . . 7
⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) |
4 | | gencbvex.2 |
. . . . . . 7
⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) |
5 | 3, 4 | anbi12d 634 |
. . . . . 6
⊢ (𝐴 = 𝑦 → ((𝜒 ∧ 𝜑) ↔ (𝜃 ∧ 𝜓))) |
6 | 5 | bicomd 226 |
. . . . 5
⊢ (𝐴 = 𝑦 → ((𝜃 ∧ 𝜓) ↔ (𝜒 ∧ 𝜑))) |
7 | 6 | eqcoms 2747 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝜃 ∧ 𝜓) ↔ (𝜒 ∧ 𝜑))) |
8 | 2, 7 | ceqsexv 3470 |
. . 3
⊢
(∃𝑦(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ (𝜒 ∧ 𝜑)) |
9 | 8 | exbii 1855 |
. 2
⊢
(∃𝑥∃𝑦(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ ∃𝑥(𝜒 ∧ 𝜑)) |
10 | | 19.41v 1958 |
. . . 4
⊢
(∃𝑥(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ (∃𝑥 𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓))) |
11 | | simpr 488 |
. . . . 5
⊢
((∃𝑥 𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) → (𝜃 ∧ 𝜓)) |
12 | | gencbvex.4 |
. . . . . . . 8
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) |
13 | | eqcom 2746 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝑦 ↔ 𝑦 = 𝐴) |
14 | 13 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑦 → 𝑦 = 𝐴) |
15 | 14 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜒 ∧ 𝐴 = 𝑦) → 𝑦 = 𝐴) |
16 | 15 | eximi 1842 |
. . . . . . . 8
⊢
(∃𝑥(𝜒 ∧ 𝐴 = 𝑦) → ∃𝑥 𝑦 = 𝐴) |
17 | 12, 16 | sylbi 220 |
. . . . . . 7
⊢ (𝜃 → ∃𝑥 𝑦 = 𝐴) |
18 | 17 | adantr 484 |
. . . . . 6
⊢ ((𝜃 ∧ 𝜓) → ∃𝑥 𝑦 = 𝐴) |
19 | 18 | ancri 553 |
. . . . 5
⊢ ((𝜃 ∧ 𝜓) → (∃𝑥 𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓))) |
20 | 11, 19 | impbii 212 |
. . . 4
⊢
((∃𝑥 𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ (𝜃 ∧ 𝜓)) |
21 | 10, 20 | bitri 278 |
. . 3
⊢
(∃𝑥(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ (𝜃 ∧ 𝜓)) |
22 | 21 | exbii 1855 |
. 2
⊢
(∃𝑦∃𝑥(𝑦 = 𝐴 ∧ (𝜃 ∧ 𝜓)) ↔ ∃𝑦(𝜃 ∧ 𝜓)) |
23 | 1, 9, 22 | 3bitr3i 304 |
1
⊢
(∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) |