Step |
Hyp |
Ref |
Expression |
1 |
|
cbvrabcsfw.1 |
|- F/_ y A |
2 |
|
cbvrabcsfw.2 |
|- F/_ x B |
3 |
|
cbvrabcsfw.3 |
|- F/ y ph |
4 |
|
cbvrabcsfw.4 |
|- F/ x ps |
5 |
|
cbvrabcsfw.5 |
|- ( x = y -> A = B ) |
6 |
|
cbvrabcsfw.6 |
|- ( x = y -> ( ph <-> ps ) ) |
7 |
|
nfv |
|- F/ z ( x e. A /\ ph ) |
8 |
|
nfcsb1v |
|- F/_ x [_ z / x ]_ A |
9 |
8
|
nfcri |
|- F/ x z e. [_ z / x ]_ A |
10 |
|
nfs1v |
|- F/ x [ z / x ] ph |
11 |
9 10
|
nfan |
|- F/ x ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) |
12 |
|
id |
|- ( x = z -> x = z ) |
13 |
|
csbeq1a |
|- ( x = z -> A = [_ z / x ]_ A ) |
14 |
12 13
|
eleq12d |
|- ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) ) |
15 |
|
sbequ12 |
|- ( x = z -> ( ph <-> [ z / x ] ph ) ) |
16 |
14 15
|
anbi12d |
|- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) ) ) |
17 |
7 11 16
|
cbvabw |
|- { x | ( x e. A /\ ph ) } = { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) } |
18 |
|
nfcv |
|- F/_ y z |
19 |
18 1
|
nfcsbw |
|- F/_ y [_ z / x ]_ A |
20 |
19
|
nfcri |
|- F/ y z e. [_ z / x ]_ A |
21 |
3
|
nfsbv |
|- F/ y [ z / x ] ph |
22 |
20 21
|
nfan |
|- F/ y ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) |
23 |
|
nfv |
|- F/ z ( y e. B /\ ps ) |
24 |
|
id |
|- ( z = y -> z = y ) |
25 |
|
csbeq1 |
|- ( z = y -> [_ z / x ]_ A = [_ y / x ]_ A ) |
26 |
|
vex |
|- y e. _V |
27 |
26 2 5
|
csbief |
|- [_ y / x ]_ A = B |
28 |
25 27
|
eqtrdi |
|- ( z = y -> [_ z / x ]_ A = B ) |
29 |
24 28
|
eleq12d |
|- ( z = y -> ( z e. [_ z / x ]_ A <-> y e. B ) ) |
30 |
4 6
|
sbhypf |
|- ( z = y -> ( [ z / x ] ph <-> ps ) ) |
31 |
29 30
|
anbi12d |
|- ( z = y -> ( ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) <-> ( y e. B /\ ps ) ) ) |
32 |
22 23 31
|
cbvabw |
|- { z | ( z e. [_ z / x ]_ A /\ [ z / x ] ph ) } = { y | ( y e. B /\ ps ) } |
33 |
17 32
|
eqtri |
|- { x | ( x e. A /\ ph ) } = { y | ( y e. B /\ ps ) } |
34 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
35 |
|
df-rab |
|- { y e. B | ps } = { y | ( y e. B /\ ps ) } |
36 |
33 34 35
|
3eqtr4i |
|- { x e. A | ph } = { y e. B | ps } |