Proof of Theorem reu3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reurex 3383 | . . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) | 
| 2 |  | reu6 3731 | . . . 4
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)) | 
| 3 |  | biimp 215 | . . . . . 6
⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦)) | 
| 4 | 3 | ralimi 3082 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | 
| 5 | 4 | reximi 3083 | . . . 4
⊢
(∃𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | 
| 6 | 2, 5 | sylbi 217 | . . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 → ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | 
| 7 | 1, 6 | jca 511 | . 2
⊢
(∃!𝑥 ∈
𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) | 
| 8 |  | rexex 3075 | . . . 4
⊢
(∃𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) | 
| 9 | 8 | anim2i 617 | . . 3
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) | 
| 10 |  | eu3v 2569 | . . . 4
⊢
(∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))) | 
| 11 |  | df-reu 3380 | . . . 4
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | 
| 12 |  | df-rex 3070 | . . . . 5
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | 
| 13 |  | df-ral 3061 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) | 
| 14 |  | impexp 450 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) | 
| 15 | 14 | albii 1818 | . . . . . . 7
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦))) | 
| 16 | 13, 15 | bitr4i 278 | . . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) | 
| 17 | 16 | exbii 1847 | . . . . 5
⊢
(∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) | 
| 18 | 12, 17 | anbi12i 628 | . . . 4
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))) | 
| 19 | 10, 11, 18 | 3bitr4i 303 | . . 3
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) | 
| 20 | 9, 19 | sylibr 234 | . 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦)) → ∃!𝑥 ∈ 𝐴 𝜑) | 
| 21 | 7, 20 | impbii 209 | 1
⊢
(∃!𝑥 ∈
𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝑦))) |