Proof of Theorem gencbvex
Step | Hyp | Ref
| Expression |
1 | | excom 1741 |
. 2
⊢ (∃x∃y(y = A ∧ (θ ∧ ψ)) ↔
∃y∃x(y = A ∧ (θ ∧ ψ))) |
2 | | gencbvex.1 |
. . . 4
⊢ A ∈
V |
3 | | gencbvex.3 |
. . . . . . 7
⊢ (A = y →
(χ ↔ θ)) |
4 | | gencbvex.2 |
. . . . . . 7
⊢ (A = y →
(φ ↔ ψ)) |
5 | 3, 4 | anbi12d 691 |
. . . . . 6
⊢ (A = y →
((χ ∧
φ) ↔ (θ ∧ ψ))) |
6 | 5 | bicomd 192 |
. . . . 5
⊢ (A = y →
((θ ∧ ψ) ↔
(χ ∧
φ))) |
7 | 6 | eqcoms 2356 |
. . . 4
⊢ (y = A →
((θ ∧ ψ) ↔
(χ ∧
φ))) |
8 | 2, 7 | ceqsexv 2894 |
. . 3
⊢ (∃y(y = A ∧ (θ ∧ ψ)) ↔
(χ ∧
φ)) |
9 | 8 | exbii 1582 |
. 2
⊢ (∃x∃y(y = A ∧ (θ ∧ ψ)) ↔
∃x(χ ∧ φ)) |
10 | | 19.41v 1901 |
. . . 4
⊢ (∃x(y = A ∧ (θ ∧ ψ)) ↔
(∃x
y = A
∧ (θ
∧ ψ))) |
11 | | simpr 447 |
. . . . 5
⊢ ((∃x y = A ∧ (θ ∧ ψ)) →
(θ ∧
ψ)) |
12 | | gencbvex.4 |
. . . . . . . 8
⊢ (θ ↔ ∃x(χ ∧ A = y)) |
13 | | eqcom 2355 |
. . . . . . . . . . 11
⊢ (A = y ↔
y = A) |
14 | 13 | biimpi 186 |
. . . . . . . . . 10
⊢ (A = y →
y = A) |
15 | 14 | adantl 452 |
. . . . . . . . 9
⊢ ((χ ∧ A = y) →
y = A) |
16 | 15 | eximi 1576 |
. . . . . . . 8
⊢ (∃x(χ ∧ A = y) →
∃x
y = A) |
17 | 12, 16 | sylbi 187 |
. . . . . . 7
⊢ (θ → ∃x y = A) |
18 | 17 | adantr 451 |
. . . . . 6
⊢ ((θ ∧ ψ) → ∃x y = A) |
19 | 18 | ancri 535 |
. . . . 5
⊢ ((θ ∧ ψ) → (∃x y = A ∧ (θ ∧ ψ))) |
20 | 11, 19 | impbii 180 |
. . . 4
⊢ ((∃x y = A ∧ (θ ∧ ψ)) ↔
(θ ∧
ψ)) |
21 | 10, 20 | bitri 240 |
. . 3
⊢ (∃x(y = A ∧ (θ ∧ ψ)) ↔
(θ ∧
ψ)) |
22 | 21 | exbii 1582 |
. 2
⊢ (∃y∃x(y = A ∧ (θ ∧ ψ)) ↔
∃y(θ ∧ ψ)) |
23 | 1, 9, 22 | 3bitr3i 266 |
1
⊢ (∃x(χ ∧ φ) ↔ ∃y(θ ∧ ψ)) |