| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eunex 5389 | . . . . 5
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥 ¬ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 2 |  | exnal 1826 | . . . . 5
⊢
(∃𝑥 ¬
∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 3 | 1, 2 | sylib 218 | . . . 4
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 4 |  | rzal 4508 | . . . . 5
⊢ (𝐴 = ∅ → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 5 | 4 | alrimiv 1926 | . . . 4
⊢ (𝐴 = ∅ → ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 6 | 3, 5 | nsyl3 138 | . . 3
⊢ (𝐴 = ∅ → ¬
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 7 | 6 | pm2.21d 121 | . 2
⊢ (𝐴 = ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 8 |  | simpr 484 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 9 |  | nfra1 3283 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑧 = 𝐵 | 
| 10 |  | nfra1 3283 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑥 = 𝐵 | 
| 11 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) | 
| 12 |  | rspa 3247 | . . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑧 = 𝐵) | 
| 13 | 12 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑧 = 𝐵) | 
| 14 | 11, 13 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢
(((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 = 𝑧) | 
| 15 |  | eqeq1 2740 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝑥 = 𝐵 ↔ 𝑧 = 𝐵)) | 
| 16 | 15 | ralbidv 3177 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑧 = 𝐵)) | 
| 17 | 16 | biimprcd 250 | . . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝐴 𝑧 = 𝐵 → (𝑥 = 𝑧 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 18 | 17 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = 𝐵) → (𝑥 = 𝑧 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 19 | 14, 18 | mpd 15 | . . . . . . . . . . . 12
⊢
(((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = 𝐵) → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 20 | 19 | exp31 419 | . . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝐴 𝑧 = 𝐵 → (𝑦 ∈ 𝐴 → (𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) | 
| 21 | 9, 10, 20 | rexlimd 3265 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 𝑧 = 𝐵 → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 22 | 21 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 23 |  | r19.2z 4494 | . . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 24 | 23 | ex 412 | . . . . . . . . . 10
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 25 | 24 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 26 | 22, 25 | impbid 212 | . . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 27 | 26 | eubidv 2585 | . . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 28 | 27 | ex 412 | . . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) | 
| 29 | 28 | exlimdv 1932 | . . . . 5
⊢ (𝐴 ≠ ∅ →
(∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) | 
| 30 |  | euex 2576 | . . . . . 6
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 31 | 16 | cbvexvw 2035 | . . . . . 6
⊢
(∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) | 
| 32 | 30, 31 | sylib 218 | . . . . 5
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) | 
| 33 | 29, 32 | impel 505 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 34 | 8, 33 | mpbird 257 | . . 3
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) | 
| 35 | 34 | ex 412 | . 2
⊢ (𝐴 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) | 
| 36 | 7, 35 | pm2.61ine 3024 | 1
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |