Step | Hyp | Ref
| Expression |
1 | | euex 1927 |
. 2
⊢ (∃!y∀x y = A →
∃y∀x y = A) |
2 | | vex 2554 |
. . . . . . 7
⊢ z ∈
V |
3 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎxz |
4 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋z / x⦌A |
5 | 4 | nfeq2 2186 |
. . . . . . . 8
⊢
Ⅎx y = ⦋z / x⦌A |
6 | | csbeq1a 2854 |
. . . . . . . . 9
⊢ (x = z →
A = ⦋z / x⦌A) |
7 | 6 | eqeq2d 2048 |
. . . . . . . 8
⊢ (x = z →
(y = A
↔ y = ⦋z / x⦌A)) |
8 | 3, 5, 7 | spcgf 2629 |
. . . . . . 7
⊢ (z ∈ V →
(∀x
y = A
→ y = ⦋z / x⦌A)) |
9 | 2, 8 | ax-mp 7 |
. . . . . 6
⊢ (∀x y = A →
y = ⦋z / x⦌A) |
10 | | vex 2554 |
. . . . . . 7
⊢ w ∈
V |
11 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎxw |
12 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋w / x⦌A |
13 | 12 | nfeq2 2186 |
. . . . . . . 8
⊢
Ⅎx y = ⦋w / x⦌A |
14 | | csbeq1a 2854 |
. . . . . . . . 9
⊢ (x = w →
A = ⦋w / x⦌A) |
15 | 14 | eqeq2d 2048 |
. . . . . . . 8
⊢ (x = w →
(y = A
↔ y = ⦋w / x⦌A)) |
16 | 11, 13, 15 | spcgf 2629 |
. . . . . . 7
⊢ (w ∈ V →
(∀x
y = A
→ y = ⦋w / x⦌A)) |
17 | 10, 16 | ax-mp 7 |
. . . . . 6
⊢ (∀x y = A →
y = ⦋w / x⦌A) |
18 | 9, 17 | eqtr3d 2071 |
. . . . 5
⊢ (∀x y = A →
⦋z / x⦌A = ⦋w / x⦌A) |
19 | 18 | alrimivv 1752 |
. . . 4
⊢ (∀x y = A →
∀z∀w⦋z / x⦌A = ⦋w / x⦌A) |
20 | | sbnfc2 2900 |
. . . 4
⊢
(ℲxA ↔ ∀z∀w⦋z / x⦌A = ⦋w / x⦌A) |
21 | 19, 20 | sylibr 137 |
. . 3
⊢ (∀x y = A →
ℲxA) |
22 | 21 | exlimiv 1486 |
. 2
⊢ (∃y∀x y = A →
ℲxA) |
23 | 1, 22 | syl 14 |
1
⊢ (∃!y∀x y = A →
ℲxA) |