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