Proof of Theorem reu3
Step | Hyp | Ref
| Expression |
1 | | reurex 2825 |
. . 3
⊢ (∃!x ∈ A φ → ∃x ∈ A φ) |
2 | | reu6 3025 |
. . . 4
⊢ (∃!x ∈ A φ ↔ ∃y ∈ A ∀x ∈ A (φ ↔ x = y)) |
3 | | bi1 178 |
. . . . . 6
⊢ ((φ ↔ x = y) →
(φ → x = y)) |
4 | 3 | ralimi 2689 |
. . . . 5
⊢ (∀x ∈ A (φ ↔ x = y) →
∀x
∈ A
(φ → x = y)) |
5 | 4 | reximi 2721 |
. . . 4
⊢ (∃y ∈ A ∀x ∈ A (φ ↔ x = y) →
∃y ∈ A ∀x ∈ A (φ → x = y)) |
6 | 2, 5 | sylbi 187 |
. . 3
⊢ (∃!x ∈ A φ → ∃y ∈ A ∀x ∈ A (φ → x = y)) |
7 | 1, 6 | jca 518 |
. 2
⊢ (∃!x ∈ A φ → (∃x ∈ A φ ∧ ∃y ∈ A ∀x ∈ A (φ → x = y))) |
8 | | rexex 2673 |
. . . 4
⊢ (∃y ∈ A ∀x ∈ A (φ → x = y) →
∃y∀x ∈ A (φ → x = y)) |
9 | 8 | anim2i 552 |
. . 3
⊢ ((∃x ∈ A φ ∧ ∃y ∈ A ∀x ∈ A (φ → x = y)) →
(∃x
∈ A φ ∧ ∃y∀x ∈ A (φ → x = y))) |
10 | | nfv 1619 |
. . . . 5
⊢ Ⅎy(x ∈ A ∧ φ) |
11 | 10 | eu3 2230 |
. . . 4
⊢ (∃!x(x ∈ A ∧ φ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃y∀x((x ∈ A ∧ φ) → x = y))) |
12 | | df-reu 2621 |
. . . 4
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
13 | | df-rex 2620 |
. . . . 5
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ)) |
14 | | df-ral 2619 |
. . . . . . 7
⊢ (∀x ∈ A (φ → x = y) ↔
∀x(x ∈ A →
(φ → x = y))) |
15 | | impexp 433 |
. . . . . . . 8
⊢ (((x ∈ A ∧ φ) → x = y) ↔
(x ∈
A → (φ → x = y))) |
16 | 15 | albii 1566 |
. . . . . . 7
⊢ (∀x((x ∈ A ∧ φ) → x = y) ↔
∀x(x ∈ A →
(φ → x = y))) |
17 | 14, 16 | bitr4i 243 |
. . . . . 6
⊢ (∀x ∈ A (φ → x = y) ↔
∀x((x ∈ A ∧ φ) →
x = y)) |
18 | 17 | exbii 1582 |
. . . . 5
⊢ (∃y∀x ∈ A (φ → x = y) ↔
∃y∀x((x ∈ A ∧ φ) → x = y)) |
19 | 13, 18 | anbi12i 678 |
. . . 4
⊢ ((∃x ∈ A φ ∧ ∃y∀x ∈ A (φ → x = y)) ↔
(∃x(x ∈ A ∧ φ) ∧ ∃y∀x((x ∈ A ∧ φ) →
x = y))) |
20 | 11, 12, 19 | 3bitr4i 268 |
. . 3
⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃y∀x ∈ A (φ → x = y))) |
21 | 9, 20 | sylibr 203 |
. 2
⊢ ((∃x ∈ A φ ∧ ∃y ∈ A ∀x ∈ A (φ → x = y)) →
∃!x
∈ A φ) |
22 | 7, 21 | impbii 180 |
1
⊢ (∃!x ∈ A φ ↔ (∃x ∈ A φ ∧ ∃y ∈ A ∀x ∈ A (φ → x = y))) |