Proof of Theorem eusv2nf
Step | Hyp | Ref
| Expression |
1 | | nfeu1 2480 |
. . . 4
⊢
Ⅎ𝑦∃!𝑦∃𝑥 𝑦 = 𝐴 |
2 | | nfe1 2027 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥 𝑦 = 𝐴 |
3 | 2 | nfeu 2486 |
. . . . . 6
⊢
Ⅎ𝑥∃!𝑦∃𝑥 𝑦 = 𝐴 |
4 | | eusv2.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
5 | 4 | isseti 3209 |
. . . . . . . 8
⊢
∃𝑦 𝑦 = 𝐴 |
6 | | 19.8a 2052 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ∃𝑥 𝑦 = 𝐴) |
7 | 6 | ancri 575 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) |
8 | 5, 7 | eximii 1764 |
. . . . . . 7
⊢
∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴) |
9 | | eupick 2536 |
. . . . . . 7
⊢
((∃!𝑦∃𝑥 𝑦 = 𝐴 ∧ ∃𝑦(∃𝑥 𝑦 = 𝐴 ∧ 𝑦 = 𝐴)) → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
10 | 8, 9 | mpan2 707 |
. . . . . 6
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → (∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
11 | 3, 10 | alrimi 2082 |
. . . . 5
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
12 | | nf6 2117 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝐴 ↔ ∀𝑥(∃𝑥 𝑦 = 𝐴 → 𝑦 = 𝐴)) |
13 | 11, 12 | sylibr 224 |
. . . 4
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
14 | 1, 13 | alrimi 2082 |
. . 3
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
15 | | dfnfc2 4454 |
. . . 4
⊢
(∀𝑥 𝐴 ∈ V →
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
16 | 15, 4 | mpg 1724 |
. . 3
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | 14, 16 | sylibr 224 |
. 2
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) |
18 | | eusvnfb 4862 |
. . . 4
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) |
19 | 4, 18 | mpbiran2 954 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |
20 | | eusv2i 4863 |
. . 3
⊢
(∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
21 | 19, 20 | sylbir 225 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) |
22 | 17, 21 | impbii 199 |
1
⊢
(∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) |