Step | Hyp | Ref
| Expression |
1 | | eunex 5008 |
. . . . 5
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥 ¬ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
2 | | exnal 1903 |
. . . . 5
⊢
(∃𝑥 ¬
∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
3 | 1, 2 | sylib 208 |
. . . 4
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ¬ ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
4 | | rzal 4217 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
5 | 4 | alrimiv 2004 |
. . . 4
⊢ (𝐴 = ∅ → ∀𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
6 | 3, 5 | nsyl3 133 |
. . 3
⊢ (𝐴 = ∅ → ¬
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
7 | 6 | pm2.21d 118 |
. 2
⊢ (𝐴 = ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
8 | | simpr 479 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
9 | | euex 2631 |
. . . . . . 7
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
10 | | eqeq1 2764 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = 𝐵 ↔ 𝑧 = 𝐵)) |
11 | 10 | ralbidv 3124 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑧 = 𝐵)) |
12 | 11 | cbvexv 2420 |
. . . . . . 7
⊢
(∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
13 | 9, 12 | sylib 208 |
. . . . . 6
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
14 | | nfv 1992 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝐴 ≠ ∅ |
15 | | nfra1 3079 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑧 = 𝐵 |
16 | 14, 15 | nfan 1977 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
17 | | nfra1 3079 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 𝑥 = 𝐵 |
18 | | simprr 813 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝐵) |
19 | | rspa 3068 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑦 ∈
𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑧 = 𝐵) |
20 | 19 | ad2ant2lr 801 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑧 = 𝐵) |
21 | 18, 20 | eqtr4d 2797 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑧) |
22 | | simplr 809 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → ∀𝑦 ∈ 𝐴 𝑧 = 𝐵) |
23 | 22, 11 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → (𝑥 = 𝑧 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
24 | 21, 23 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵)) → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵) |
25 | 24 | exp32 632 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (𝑦 ∈ 𝐴 → (𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
26 | 16, 17, 25 | rexlimd 3164 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
27 | | r19.2z 4204 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |
28 | 27 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
29 | 28 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
30 | 26, 29 | impbid 202 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
31 | 30 | eubidv 2627 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑧 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
32 | 31 | ex 449 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
33 | 32 | exlimdv 2010 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∃𝑧∀𝑦 ∈ 𝐴 𝑧 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
34 | 13, 33 | syl5 34 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))) |
35 | 34 | imp 444 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
36 | 8, 35 | mpbird 247 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |
37 | 36 | ex 449 |
. 2
⊢ (𝐴 ≠ ∅ →
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵)) |
38 | 7, 37 | pm2.61ine 3015 |
1
⊢
(∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) |