Proof of Theorem reu3
Step | Hyp | Ref
| Expression |
1 | | reurex 2670 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) |
2 | | reu6 2901 |
. . . 4
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)) |
3 | | biimp 117 |
. . . . . 6
⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦)) |
4 | 3 | ralimi 2520 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) |
5 | 4 | reximi 2554 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) |
6 | 2, 5 | sylbi 120 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) |
7 | 1, 6 | jca 304 |
. 2
⊢
(∃!𝑥 ∈
𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) |
8 | | rexex 2503 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) |
9 | 8 | anim2i 340 |
. . 3
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) |
10 | | nfv 1508 |
. . . . 5
⊢
Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) |
11 | 10 | eu3 2052 |
. . . 4
⊢
(∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))) |
12 | | df-reu 2442 |
. . . 4
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
13 | | df-rex 2441 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
14 | | df-ral 2440 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) |
15 | | impexp 261 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) |
16 | 15 | albii 1450 |
. . . . . . 7
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) |
17 | 14, 16 | bitr4i 186 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) |
18 | 17 | exbii 1585 |
. . . . 5
⊢
(∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) |
19 | 13, 18 | anbi12i 456 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))) |
20 | 11, 12, 19 | 3bitr4i 211 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) |
21 | 9, 20 | sylibr 133 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → ∃!𝑥 ∈ 𝐴 𝜑) |
22 | 7, 21 | impbii 125 |
1
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) |