Step | Hyp | Ref
| Expression |
1 | | nfv 1619 |
. . . 4
⊢ Ⅎz(x ∈ A ∧ φ) |
2 | | nfcsb1v 3168 |
. . . . . 6
⊢
Ⅎx[z / x]A |
3 | 2 | nfcri 2483 |
. . . . 5
⊢ Ⅎx z ∈ [z /
x]A |
4 | | nfs1v 2106 |
. . . . 5
⊢ Ⅎx[z / x]φ |
5 | 3, 4 | nfan 1824 |
. . . 4
⊢ Ⅎx(z ∈ [z /
x]A ∧ [z / x]φ) |
6 | | id 19 |
. . . . . 6
⊢ (x = z →
x = z) |
7 | | csbeq1a 3144 |
. . . . . 6
⊢ (x = z →
A = [z / x]A) |
8 | 6, 7 | eleq12d 2421 |
. . . . 5
⊢ (x = z →
(x ∈
A ↔ z ∈
[z / x]A)) |
9 | | sbequ12 1919 |
. . . . 5
⊢ (x = z →
(φ ↔ [z / x]φ)) |
10 | 8, 9 | anbi12d 691 |
. . . 4
⊢ (x = z →
((x ∈
A ∧ φ) ↔ (z ∈
[z / x]A ∧ [z / x]φ))) |
11 | 1, 5, 10 | cbveu 2224 |
. . 3
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃!z(z ∈
[z / x]A ∧ [z / x]φ)) |
12 | | nfcv 2489 |
. . . . . . 7
⊢
Ⅎyz |
13 | | cbvralcsf.1 |
. . . . . . 7
⊢
ℲyA |
14 | 12, 13 | nfcsb 3170 |
. . . . . 6
⊢
Ⅎy[z / x]A |
15 | 14 | nfcri 2483 |
. . . . 5
⊢ Ⅎy z ∈ [z /
x]A |
16 | | cbvralcsf.3 |
. . . . . 6
⊢ Ⅎyφ |
17 | 16 | nfsb 2109 |
. . . . 5
⊢ Ⅎy[z / x]φ |
18 | 15, 17 | nfan 1824 |
. . . 4
⊢ Ⅎy(z ∈ [z /
x]A ∧ [z / x]φ) |
19 | | nfv 1619 |
. . . 4
⊢ Ⅎz(y ∈ B ∧ ψ) |
20 | | id 19 |
. . . . . 6
⊢ (z = y →
z = y) |
21 | | csbeq1 3139 |
. . . . . . 7
⊢ (z = y →
[z / x]A =
[y / x]A) |
22 | | sbsbc 3050 |
. . . . . . . . 9
⊢ ([y / x]v ∈ A ↔ [̣y / x]̣v ∈ A) |
23 | 22 | abbii 2465 |
. . . . . . . 8
⊢ {v ∣ [y / x]v ∈ A} = {v ∣ [̣y /
x]̣v ∈ A} |
24 | | cbvralcsf.2 |
. . . . . . . . . . . 12
⊢
ℲxB |
25 | 24 | nfcri 2483 |
. . . . . . . . . . 11
⊢ Ⅎx v ∈ B |
26 | | cbvralcsf.5 |
. . . . . . . . . . . 12
⊢ (x = y →
A = B) |
27 | 26 | eleq2d 2420 |
. . . . . . . . . . 11
⊢ (x = y →
(v ∈
A ↔ v ∈ B)) |
28 | 25, 27 | sbie 2038 |
. . . . . . . . . 10
⊢ ([y / x]v ∈ A ↔ v ∈ B) |
29 | 28 | bicomi 193 |
. . . . . . . . 9
⊢ (v ∈ B ↔ [y /
x]v
∈ A) |
30 | 29 | abbi2i 2464 |
. . . . . . . 8
⊢ B = {v ∣ [y /
x]v
∈ A} |
31 | | df-csb 3137 |
. . . . . . . 8
⊢ [y / x]A =
{v ∣
[̣y / x]̣v ∈ A} |
32 | 23, 30, 31 | 3eqtr4ri 2384 |
. . . . . . 7
⊢ [y / x]A =
B |
33 | 21, 32 | syl6eq 2401 |
. . . . . 6
⊢ (z = y →
[z / x]A =
B) |
34 | 20, 33 | eleq12d 2421 |
. . . . 5
⊢ (z = y →
(z ∈
[z / x]A
↔ y ∈ B)) |
35 | | sbequ 2060 |
. . . . . 6
⊢ (z = y →
([z / x]φ ↔
[y / x]φ)) |
36 | | cbvralcsf.4 |
. . . . . . 7
⊢ Ⅎxψ |
37 | | cbvralcsf.6 |
. . . . . . 7
⊢ (x = y →
(φ ↔ ψ)) |
38 | 36, 37 | sbie 2038 |
. . . . . 6
⊢ ([y / x]φ ↔ ψ) |
39 | 35, 38 | syl6bb 252 |
. . . . 5
⊢ (z = y →
([z / x]φ ↔
ψ)) |
40 | 34, 39 | anbi12d 691 |
. . . 4
⊢ (z = y →
((z ∈
[z / x]A ∧ [z / x]φ) ↔
(y ∈
B ∧ ψ))) |
41 | 18, 19, 40 | cbveu 2224 |
. . 3
⊢ (∃!z(z ∈
[z / x]A ∧ [z / x]φ) ↔
∃!y(y ∈ B ∧ ψ)) |
42 | 11, 41 | bitri 240 |
. 2
⊢ (∃!x(x ∈ A ∧ φ) ↔ ∃!y(y ∈ B ∧ ψ)) |
43 | | df-reu 2621 |
. 2
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
44 | | df-reu 2621 |
. 2
⊢ (∃!y ∈ B ψ ↔ ∃!y(y ∈ B ∧ ψ)) |
45 | 42, 43, 44 | 3bitr4i 268 |
1
⊢ (∃!x ∈ A φ ↔ ∃!y ∈ B ψ) |