Step |
Hyp |
Ref |
Expression |
1 |
|
ralima.x |
|- ( x = ( F ` y ) -> ( ph <-> ps ) ) |
2 |
1
|
notbid |
|- ( x = ( F ` y ) -> ( -. ph <-> -. ps ) ) |
3 |
2
|
ralima |
|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) -. ph <-> A. y e. B -. ps ) ) |
4 |
3
|
notbid |
|- ( ( F Fn A /\ B C_ A ) -> ( -. A. x e. ( F " B ) -. ph <-> -. A. y e. B -. ps ) ) |
5 |
|
dfrex2 |
|- ( E. x e. ( F " B ) ph <-> -. A. x e. ( F " B ) -. ph ) |
6 |
|
dfrex2 |
|- ( E. y e. B ps <-> -. A. y e. B -. ps ) |
7 |
4 5 6
|
3bitr4g |
|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) ) |