Step |
Hyp |
Ref |
Expression |
1 |
|
rngop.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
|
reldmoprab |
|- Rel dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
3 |
|
df-mpo |
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
4 |
1 3
|
eqtri |
|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
5 |
4
|
dmeqi |
|- dom F = dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
6 |
5
|
releqi |
|- ( Rel dom F <-> Rel dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } ) |
7 |
2 6
|
mpbir |
|- Rel dom F |