Step | Hyp | Ref
| Expression |
1 | | eunex 4785 |
. . . . 5
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥 ¬ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
2 | | exnal 1744 |
. . . . 5
⊢
(∃𝑥 ¬
∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
3 | 1, 2 | sylib 207 |
. . . 4
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
4 | | rzal 4025 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
5 | 4 | alrimiv 1842 |
. . . 4
⊢ (𝐴 = ∅ → ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
6 | 3, 5 | nsyl3 132 |
. . 3
⊢ (𝐴 = ∅ → ¬
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
7 | 6 | pm2.21d 117 |
. 2
⊢ (𝐴 = ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
8 | | simpr 476 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
9 | | euex 2482 |
. . . . . . 7
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
10 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = 𝐵 ↔ 𝑧 = 𝐵)) |
11 | 10 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑧 = 𝐵)) |
12 | 11 | cbvexv 2263 |
. . . . . . 7
⊢
(∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
13 | 9, 12 | sylib 207 |
. . . . . 6
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
14 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝐴 ≠ ∅ |
15 | | nfra1 2925 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑧 = 𝐵 |
16 | 14, 15 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
17 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑥 = 𝐵 |
18 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝐵) |
19 | | rspa 2914 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑧 = 𝐵) |
20 | 19 | ad2ant2lr 780 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑧 = 𝐵) |
21 | 18, 20 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑧) |
22 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → ∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
23 | 22, 11 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → (𝑥 = 𝑧 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
24 | 21, 23 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
25 | 24 | exp32 629 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (𝑦 ∈ 𝐴 → (𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
26 | 16, 17, 25 | rexlimd 3008 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
27 | | r19.2z 4012 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |
28 | 27 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
29 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
30 | 26, 29 | impbid 201 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
31 | 30 | eubidv 2478 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
32 | 31 | ex 449 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
33 | 32 | exlimdv 1848 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
34 | 13, 33 | syl5 33 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
35 | 34 | imp 444 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
36 | 8, 35 | mpbird 246 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |
37 | 36 | ex 449 |
. 2
⊢ (𝐴 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
38 | 7, 37 | pm2.61ine 2865 |
1
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |