Step | Hyp | Ref
| Expression |
1 | | reu3 3626 |
. 2
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧))) |
2 | | rmo4.1 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
3 | | equequ1 2037 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
4 | | equcom 2030 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 ↔ 𝑧 = 𝑦) |
5 | 3, 4 | bitrdi 290 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑧 = 𝑦)) |
6 | 2, 5 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑧 = 𝑦))) |
7 | 6 | cbvralvw 3349 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦)) |
8 | 7 | rexbii 3161 |
. . . 4
⊢
(∃𝑧 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦)) |
9 | | equequ1 2037 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 ↔ 𝑥 = 𝑦)) |
10 | 9 | imbi2d 344 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝜓 → 𝑧 = 𝑦) ↔ (𝜓 → 𝑥 = 𝑦))) |
11 | 10 | ralbidv 3109 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
12 | 11 | cbvrexvw 3350 |
. . . 4
⊢
(∃𝑧 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
13 | 8, 12 | bitri 278 |
. . 3
⊢
(∃𝑧 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
14 | 13 | anbi2i 626 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
15 | 1, 14 | bitri 278 |
1
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |