Step |
Hyp |
Ref |
Expression |
1 |
|
wfis2fg.1 |
|- F/ y ps |
2 |
|
wfis2fg.2 |
|- ( y = z -> ( ph <-> ps ) ) |
3 |
|
wfis2fg.3 |
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) ) |
4 |
|
sbsbc |
|- ( [ z / y ] ph <-> [. z / y ]. ph ) |
5 |
1 2
|
sbiev |
|- ( [ z / y ] ph <-> ps ) |
6 |
4 5
|
bitr3i |
|- ( [. z / y ]. ph <-> ps ) |
7 |
6
|
ralbii |
|- ( A. z e. Pred ( R , A , y ) [. z / y ]. ph <-> A. z e. Pred ( R , A , y ) ps ) |
8 |
7 3
|
syl5bi |
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) |
9 |
8
|
wfisg |
|- ( ( R We A /\ R Se A ) -> A. y e. A ph ) |