Metamath Proof Explorer


Theorem reldmmpo

Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypothesis rngop.1
|- F = ( x e. A , y e. B |-> C )
Assertion reldmmpo
|- Rel dom F

Proof

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