Theorem rnmpo

Description: The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011)

	Ref	Expression
Hypothesis	rngop.1	|- F = ( x e. A , y e. B |-> C )
Assertion	rnmpo	|- ran F = { z | E. x e. A E. y e. B z = C }

Proof

Step	Hyp	Ref	Expression
1		rngop.1	|- F = ( x e. A , y e. B |-> C )
2		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3	1 2	eqtri	|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
4	3	rneqi	|- ran F = ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
5		rnoprab2	|- ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { z | E. x e. A E. y e. B z = C }
6	4 5	eqtri	|- ran F = { z | E. x e. A E. y e. B z = C }