Step |
Hyp |
Ref |
Expression |
1 |
|
frinsg.1 |
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) |
2 |
|
ssrab2 |
|- { y e. A | ph } C_ A |
3 |
|
dfss3 |
|- ( Pred ( R , A , w ) C_ { y e. A | ph } <-> A. z e. Pred ( R , A , w ) z e. { y e. A | ph } ) |
4 |
|
nfcv |
|- F/_ y A |
5 |
4
|
elrabsf |
|- ( z e. { y e. A | ph } <-> ( z e. A /\ [. z / y ]. ph ) ) |
6 |
5
|
simprbi |
|- ( z e. { y e. A | ph } -> [. z / y ]. ph ) |
7 |
6
|
ralimi |
|- ( A. z e. Pred ( R , A , w ) z e. { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) |
8 |
3 7
|
sylbi |
|- ( Pred ( R , A , w ) C_ { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) |
9 |
|
nfv |
|- F/ y w e. A |
10 |
|
nfcv |
|- F/_ y Pred ( R , A , w ) |
11 |
|
nfsbc1v |
|- F/ y [. z / y ]. ph |
12 |
10 11
|
nfralw |
|- F/ y A. z e. Pred ( R , A , w ) [. z / y ]. ph |
13 |
|
nfsbc1v |
|- F/ y [. w / y ]. ph |
14 |
12 13
|
nfim |
|- F/ y ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) |
15 |
9 14
|
nfim |
|- F/ y ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) |
16 |
|
eleq1w |
|- ( y = w -> ( y e. A <-> w e. A ) ) |
17 |
|
predeq3 |
|- ( y = w -> Pred ( R , A , y ) = Pred ( R , A , w ) ) |
18 |
17
|
raleqdv |
|- ( y = w -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph <-> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) ) |
19 |
|
sbceq1a |
|- ( y = w -> ( ph <-> [. w / y ]. ph ) ) |
20 |
18 19
|
imbi12d |
|- ( y = w -> ( ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) <-> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) |
21 |
16 20
|
imbi12d |
|- ( y = w -> ( ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) <-> ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) ) |
22 |
15 21 1
|
chvarfv |
|- ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) |
23 |
8 22
|
syl5 |
|- ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> [. w / y ]. ph ) ) |
24 |
23
|
anc2li |
|- ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> ( w e. A /\ [. w / y ]. ph ) ) ) |
25 |
4
|
elrabsf |
|- ( w e. { y e. A | ph } <-> ( w e. A /\ [. w / y ]. ph ) ) |
26 |
24 25
|
syl6ibr |
|- ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) |
27 |
26
|
rgen |
|- A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) |
28 |
|
frind |
|- ( ( ( R Fr A /\ R Se A ) /\ ( { y e. A | ph } C_ A /\ A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) ) -> A = { y e. A | ph } ) |
29 |
2 27 28
|
mpanr12 |
|- ( ( R Fr A /\ R Se A ) -> A = { y e. A | ph } ) |
30 |
|
rabid2 |
|- ( A = { y e. A | ph } <-> A. y e. A ph ) |
31 |
29 30
|
sylib |
|- ( ( R Fr A /\ R Se A ) -> A. y e. A ph ) |