Proof of Theorem euxfr2dc
Step | Hyp | Ref
| Expression |
1 | | euxfr2dc.2 |
. . . . . . 7
⊢ ∃*y x = A |
2 | 1 | moani 1967 |
. . . . . 6
⊢ ∃*y(φ ∧ x = A) |
3 | | ancom 253 |
. . . . . . 7
⊢ ((φ ∧ x = A) ↔
(x = A
∧ φ)) |
4 | 3 | mobii 1934 |
. . . . . 6
⊢ (∃*y(φ ∧ x = A) ↔
∃*y(x = A ∧ φ)) |
5 | 2, 4 | mpbi 133 |
. . . . 5
⊢ ∃*y(x = A ∧ φ) |
6 | 5 | ax-gen 1335 |
. . . 4
⊢ ∀x∃*y(x = A ∧ φ) |
7 | | excom 1551 |
. . . . . 6
⊢ (∃y∃x(x = A ∧ φ) ↔
∃x∃y(x = A ∧ φ)) |
8 | 7 | dcbii 746 |
. . . . 5
⊢
(DECID ∃y∃x(x = A ∧ φ) ↔ DECID ∃x∃y(x = A ∧ φ)) |
9 | | 2euswapdc 1988 |
. . . . 5
⊢
(DECID ∃x∃y(x = A ∧ φ) → (∀x∃*y(x = A ∧ φ) →
(∃!x∃y(x = A ∧ φ) → ∃!y∃x(x = A ∧ φ)))) |
10 | 8, 9 | sylbi 114 |
. . . 4
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∀x∃*y(x = A ∧ φ) →
(∃!x∃y(x = A ∧ φ) → ∃!y∃x(x = A ∧ φ)))) |
11 | 6, 10 | mpi 15 |
. . 3
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∃!x∃y(x = A ∧ φ) →
∃!y∃x(x = A ∧ φ))) |
12 | | moeq 2710 |
. . . . . . 7
⊢ ∃*x x = A |
13 | 12 | moani 1967 |
. . . . . 6
⊢ ∃*x(φ ∧ x = A) |
14 | 3 | mobii 1934 |
. . . . . 6
⊢ (∃*x(φ ∧ x = A) ↔
∃*x(x = A ∧ φ)) |
15 | 13, 14 | mpbi 133 |
. . . . 5
⊢ ∃*x(x = A ∧ φ) |
16 | 15 | ax-gen 1335 |
. . . 4
⊢ ∀y∃*x(x = A ∧ φ) |
17 | | 2euswapdc 1988 |
. . . 4
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∀y∃*x(x = A ∧ φ) →
(∃!y∃x(x = A ∧ φ) → ∃!x∃y(x = A ∧ φ)))) |
18 | 16, 17 | mpi 15 |
. . 3
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∃!y∃x(x = A ∧ φ) →
∃!x∃y(x = A ∧ φ))) |
19 | 11, 18 | impbid 120 |
. 2
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∃!x∃y(x = A ∧ φ) ↔
∃!y∃x(x = A ∧ φ))) |
20 | | euxfr2dc.1 |
. . . 4
⊢ A ∈
V |
21 | | biidd 161 |
. . . 4
⊢ (x = A →
(φ ↔ φ)) |
22 | 20, 21 | ceqsexv 2587 |
. . 3
⊢ (∃x(x = A ∧ φ) ↔
φ) |
23 | 22 | eubii 1906 |
. 2
⊢ (∃!y∃x(x = A ∧ φ) ↔
∃!yφ) |
24 | 19, 23 | syl6bb 185 |
1
⊢
(DECID ∃y∃x(x = A ∧ φ) → (∃!x∃y(x = A ∧ φ) ↔
∃!yφ)) |