Proof of Theorem eusv2nf
Step | Hyp | Ref
| Expression |
1 | | nfeu1 2017 |
. . . 4
⊢
Ⅎ𝑦∃!𝑦∃𝑥 𝑦 = 𝐴 |
2 | | nfe1 1476 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥 𝑦 = 𝐴 |
3 | 2 | nfeu 2025 |
. . . . . 6
⊢
Ⅎ𝑥∃!𝑦∃𝑥 𝑦 = 𝐴 |
4 | | eusv2.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
5 | 4 | isseti 2720 |
. . . . . . . 8
⊢
∃𝑦 𝑦 = 𝐴 |
6 | | 19.8a 1570 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴) |
7 | 6 | ancri 322 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) |
8 | 5, 7 | eximii 1582 |
. . . . . . 7
⊢
∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴) |
9 | | eupick 2085 |
. . . . . . 7
⊢
((∃!𝑦∃𝑥 𝑦 = 𝐴 ∧ ∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
10 | 8, 9 | mpan2 422 |
. . . . . 6
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
11 | 3, 10 | alrimi 1502 |
. . . . 5
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
12 | | nf3 1649 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝐴 ↔ ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
13 | 11, 12 | sylibr 133 |
. . . 4
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
14 | 1, 13 | alrimi 1502 |
. . 3
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
15 | | dfnfc2 3790 |
. . . 4
⊢
(∀𝑥 𝐴 ∈ V →
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
16 | 15, 4 | mpg 1431 |
. . 3
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | 14, 16 | sylibr 133 |
. 2
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) |
18 | | eusvnfb 4414 |
. . . 4
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) |
19 | 4, 18 | mpbiran2 926 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |
20 | | eusv2i 4415 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
21 | 19, 20 | sylbir 134 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
22 | 17, 21 | impbii 125 |
1
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |