Proof of Theorem eusv2nf
Step | Hyp | Ref
| Expression |
1 | | nfeu1 1911 |
. . . 4
⊢
Ⅎ𝑦∃!𝑦∃𝑥 𝑦 = 𝐴 |
2 | | nfe1 1385 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥 𝑦 = 𝐴 |
3 | 2 | nfeu 1919 |
. . . . . 6
⊢
Ⅎ𝑥∃!𝑦∃𝑥 𝑦 = 𝐴 |
4 | | eusv2.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
5 | 4 | isseti 2563 |
. . . . . . . 8
⊢
∃𝑦 𝑦 = 𝐴 |
6 | | 19.8a 1482 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴) |
7 | 6 | ancri 307 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) |
8 | 5, 7 | eximii 1493 |
. . . . . . 7
⊢
∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴) |
9 | | eupick 1979 |
. . . . . . 7
⊢
((∃!𝑦∃𝑥 𝑦 = 𝐴 ∧ ∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
10 | 8, 9 | mpan2 401 |
. . . . . 6
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
11 | 3, 10 | alrimi 1415 |
. . . . 5
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
12 | | nf3 1559 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝐴 ↔ ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
13 | 11, 12 | sylibr 137 |
. . . 4
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
14 | 1, 13 | alrimi 1415 |
. . 3
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
15 | | dfnfc2 3598 |
. . . 4
⊢
(∀𝑥 𝐴 ∈ V →
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
16 | 15, 4 | mpg 1340 |
. . 3
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | 14, 16 | sylibr 137 |
. 2
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) |
18 | | eusvnfb 4186 |
. . . 4
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) |
19 | 4, 18 | mpbiran2 848 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |
20 | | eusv2i 4187 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
21 | 19, 20 | sylbir 125 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
22 | 17, 21 | impbii 117 |
1
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |