Proof of Theorem reupick2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ancr 546 | . . . . . 6
⊢ ((𝜓 → 𝜑) → (𝜓 → (𝜑 ∧ 𝜓))) | 
| 2 | 1 | ralimi 3083 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓))) | 
| 3 |  | rexim 3087 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) | 
| 5 |  | reupick3 4330 | . . . . . 6
⊢
((∃!𝑥 ∈
𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | 
| 6 | 5 | 3exp 1120 | . . . . 5
⊢
(∃!𝑥 ∈
𝐴 𝜑 → (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))) | 
| 7 | 6 | com12 32 | . . . 4
⊢
(∃𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) → (∃!𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))) | 
| 8 | 4, 7 | syl6 35 | . . 3
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → (∃𝑥 ∈ 𝐴 𝜓 → (∃!𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))))) | 
| 9 | 8 | 3imp1 1348 | . 2
⊢
(((∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | 
| 10 |  | rsp 3247 | . . . 4
⊢
(∀𝑥 ∈
𝐴 (𝜓 → 𝜑) → (𝑥 ∈ 𝐴 → (𝜓 → 𝜑))) | 
| 11 | 10 | 3ad2ant1 1134 | . . 3
⊢
((∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝑥 ∈ 𝐴 → (𝜓 → 𝜑))) | 
| 12 | 11 | imp 406 | . 2
⊢
(((∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜑)) | 
| 13 | 9, 12 | impbid 212 | 1
⊢
(((∀𝑥 ∈
𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) |