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

Metamath Proof Explorer

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 }