Step |
Hyp |
Ref |
Expression |
1 |
|
tfis.1 |
|- ( x e. On -> ( A. y e. x [ y / x ] ph -> ph ) ) |
2 |
|
ssrab2 |
|- { x e. On | ph } C_ On |
3 |
|
nfcv |
|- F/_ x z |
4 |
|
nfrab1 |
|- F/_ x { x e. On | ph } |
5 |
3 4
|
nfss |
|- F/ x z C_ { x e. On | ph } |
6 |
4
|
nfcri |
|- F/ x z e. { x e. On | ph } |
7 |
5 6
|
nfim |
|- F/ x ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) |
8 |
|
dfss3 |
|- ( x C_ { x e. On | ph } <-> A. y e. x y e. { x e. On | ph } ) |
9 |
|
sseq1 |
|- ( x = z -> ( x C_ { x e. On | ph } <-> z C_ { x e. On | ph } ) ) |
10 |
8 9
|
bitr3id |
|- ( x = z -> ( A. y e. x y e. { x e. On | ph } <-> z C_ { x e. On | ph } ) ) |
11 |
|
rabid |
|- ( x e. { x e. On | ph } <-> ( x e. On /\ ph ) ) |
12 |
|
eleq1w |
|- ( x = z -> ( x e. { x e. On | ph } <-> z e. { x e. On | ph } ) ) |
13 |
11 12
|
bitr3id |
|- ( x = z -> ( ( x e. On /\ ph ) <-> z e. { x e. On | ph } ) ) |
14 |
10 13
|
imbi12d |
|- ( x = z -> ( ( A. y e. x y e. { x e. On | ph } -> ( x e. On /\ ph ) ) <-> ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) ) |
15 |
|
sbequ |
|- ( w = y -> ( [ w / x ] ph <-> [ y / x ] ph ) ) |
16 |
|
nfcv |
|- F/_ x On |
17 |
|
nfcv |
|- F/_ w On |
18 |
|
nfv |
|- F/ w ph |
19 |
|
nfs1v |
|- F/ x [ w / x ] ph |
20 |
|
sbequ12 |
|- ( x = w -> ( ph <-> [ w / x ] ph ) ) |
21 |
16 17 18 19 20
|
cbvrabw |
|- { x e. On | ph } = { w e. On | [ w / x ] ph } |
22 |
15 21
|
elrab2 |
|- ( y e. { x e. On | ph } <-> ( y e. On /\ [ y / x ] ph ) ) |
23 |
22
|
simprbi |
|- ( y e. { x e. On | ph } -> [ y / x ] ph ) |
24 |
23
|
ralimi |
|- ( A. y e. x y e. { x e. On | ph } -> A. y e. x [ y / x ] ph ) |
25 |
24 1
|
syl5 |
|- ( x e. On -> ( A. y e. x y e. { x e. On | ph } -> ph ) ) |
26 |
25
|
anc2li |
|- ( x e. On -> ( A. y e. x y e. { x e. On | ph } -> ( x e. On /\ ph ) ) ) |
27 |
3 7 14 26
|
vtoclgaf |
|- ( z e. On -> ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) |
28 |
27
|
rgen |
|- A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) |
29 |
|
tfi |
|- ( ( { x e. On | ph } C_ On /\ A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) -> { x e. On | ph } = On ) |
30 |
2 28 29
|
mp2an |
|- { x e. On | ph } = On |
31 |
30
|
eqcomi |
|- On = { x e. On | ph } |
32 |
31
|
rabeq2i |
|- ( x e. On <-> ( x e. On /\ ph ) ) |
33 |
32
|
simprbi |
|- ( x e. On -> ph ) |