This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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