Step |
Hyp |
Ref |
Expression |
1 |
|
rngop.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
|
ralrnmpo.2 |
|- ( z = C -> ( ph <-> ps ) ) |
3 |
2
|
notbid |
|- ( z = C -> ( -. ph <-> -. ps ) ) |
4 |
1 3
|
ralrnmpo |
|- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F -. ph <-> A. x e. A A. y e. B -. ps ) ) |
5 |
4
|
notbid |
|- ( A. x e. A A. y e. B C e. V -> ( -. A. z e. ran F -. ph <-> -. A. x e. A A. y e. B -. ps ) ) |
6 |
|
dfrex2 |
|- ( E. z e. ran F ph <-> -. A. z e. ran F -. ph ) |
7 |
|
dfrex2 |
|- ( E. y e. B ps <-> -. A. y e. B -. ps ) |
8 |
7
|
rexbii |
|- ( E. x e. A E. y e. B ps <-> E. x e. A -. A. y e. B -. ps ) |
9 |
|
rexnal |
|- ( E. x e. A -. A. y e. B -. ps <-> -. A. x e. A A. y e. B -. ps ) |
10 |
8 9
|
bitri |
|- ( E. x e. A E. y e. B ps <-> -. A. x e. A A. y e. B -. ps ) |
11 |
5 6 10
|
3bitr4g |
|- ( A. x e. A A. y e. B C e. V -> ( E. z e. ran F ph <-> E. x e. A E. y e. B ps ) ) |