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 }