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

Metamath Proof Explorer

Theorem rnmpt

Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 
|- F = ( x e. A |-> B )
Assertion rnmpt 
|- ran F = { y | E. x e. A y = B }

Proof

Step Hyp Ref Expression
1 rnmpt.1 
 |-  F = ( x e. A |-> B )
2 rnopab 
 |-  ran { <. x , y >. | ( x e. A /\ y = B ) } = { y | E. x ( x e. A /\ y = B ) }
3 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4 1 3 eqtri 
 |-  F = { <. x , y >. | ( x e. A /\ y = B ) }
5 4 rneqi 
 |-  ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6 df-rex 
 |-  ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7 6 abbii 
 |-  { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8 2 5 7 3eqtr4i 
 |-  ran F = { y | E. x e. A y = B }