Step |
Hyp |
Ref |
Expression |
1 |
|
setinds.1 |
|- ( A. y e. x [. y / x ]. ph -> ph ) |
2 |
|
vex |
|- x e. _V |
3 |
|
setind |
|- ( A. z ( z C_ { x | ph } -> z e. { x | ph } ) -> { x | ph } = _V ) |
4 |
|
dfss3 |
|- ( z C_ { x | ph } <-> A. y e. z y e. { x | ph } ) |
5 |
|
df-sbc |
|- ( [. y / x ]. ph <-> y e. { x | ph } ) |
6 |
5
|
ralbii |
|- ( A. y e. z [. y / x ]. ph <-> A. y e. z y e. { x | ph } ) |
7 |
|
nfcv |
|- F/_ x z |
8 |
|
nfsbc1v |
|- F/ x [. y / x ]. ph |
9 |
7 8
|
nfralw |
|- F/ x A. y e. z [. y / x ]. ph |
10 |
|
nfsbc1v |
|- F/ x [. z / x ]. ph |
11 |
9 10
|
nfim |
|- F/ x ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) |
12 |
|
raleq |
|- ( x = z -> ( A. y e. x [. y / x ]. ph <-> A. y e. z [. y / x ]. ph ) ) |
13 |
|
sbceq1a |
|- ( x = z -> ( ph <-> [. z / x ]. ph ) ) |
14 |
12 13
|
imbi12d |
|- ( x = z -> ( ( A. y e. x [. y / x ]. ph -> ph ) <-> ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) ) ) |
15 |
11 14 1
|
chvarfv |
|- ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) |
16 |
6 15
|
sylbir |
|- ( A. y e. z y e. { x | ph } -> [. z / x ]. ph ) |
17 |
4 16
|
sylbi |
|- ( z C_ { x | ph } -> [. z / x ]. ph ) |
18 |
|
df-sbc |
|- ( [. z / x ]. ph <-> z e. { x | ph } ) |
19 |
17 18
|
sylib |
|- ( z C_ { x | ph } -> z e. { x | ph } ) |
20 |
3 19
|
mpg |
|- { x | ph } = _V |
21 |
20
|
eqcomi |
|- _V = { x | ph } |
22 |
21
|
abeq2i |
|- ( x e. _V <-> ph ) |
23 |
2 22
|
mpbi |
|- ph |