Step | Hyp | Ref
| Expression |
1 | | reu3 3662 |
. 2
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧))) |
2 | | rmo4.1 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
3 | | equequ1 2028 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
4 | | equcom 2021 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 ↔ 𝑧 = 𝑦) |
5 | 3, 4 | bitrdi 287 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑧 = 𝑦)) |
6 | 2, 5 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑧 = 𝑦))) |
7 | 6 | cbvralvw 3383 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦)) |
8 | 7 | rexbii 3181 |
. . . 4
⊢
(∃𝑧 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦)) |
9 | | equequ1 2028 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 ↔ 𝑥 = 𝑦)) |
10 | 9 | imbi2d 341 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝜓 → 𝑧 = 𝑦) ↔ (𝜓 → 𝑥 = 𝑦))) |
11 | 10 | ralbidv 3112 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
12 | 11 | cbvrexvw 3384 |
. . . 4
⊢
(∃𝑧 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
13 | 8, 12 | bitri 274 |
. . 3
⊢
(∃𝑧 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) |
14 | 13 | anbi2i 623 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |
15 | 1, 14 | bitri 274 |
1
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))) |