Proof of Theorem eusv2nf
Step | Hyp | Ref
| Expression |
1 | | nfeu1 2030 |
. . . 4
⊢
Ⅎ𝑦∃!𝑦∃𝑥 𝑦 = 𝐴 |
2 | | nfe1 1489 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥 𝑦 = 𝐴 |
3 | 2 | nfeu 2038 |
. . . . . 6
⊢
Ⅎ𝑥∃!𝑦∃𝑥 𝑦 = 𝐴 |
4 | | eusv2.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
5 | 4 | isseti 2738 |
. . . . . . . 8
⊢
∃𝑦 𝑦 = 𝐴 |
6 | | 19.8a 1583 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴) |
7 | 6 | ancri 322 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) |
8 | 5, 7 | eximii 1595 |
. . . . . . 7
⊢
∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴) |
9 | | eupick 2098 |
. . . . . . 7
⊢
((∃!𝑦∃𝑥 𝑦 = 𝐴 ∧ ∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
10 | 8, 9 | mpan2 423 |
. . . . . 6
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
11 | 3, 10 | alrimi 1515 |
. . . . 5
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
12 | | nf3 1662 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝐴 ↔ ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
13 | 11, 12 | sylibr 133 |
. . . 4
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
14 | 1, 13 | alrimi 1515 |
. . 3
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
15 | | dfnfc2 3814 |
. . . 4
⊢
(∀𝑥 𝐴 ∈ V →
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
16 | 15, 4 | mpg 1444 |
. . 3
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | 14, 16 | sylibr 133 |
. 2
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) |
18 | | eusvnfb 4439 |
. . . 4
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) |
19 | 4, 18 | mpbiran2 936 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |
20 | | eusv2i 4440 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
21 | 19, 20 | sylbir 134 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
22 | 17, 21 | impbii 125 |
1
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |