Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	dfmpt.1	|- B e. _V
Assertion	fnasrn	|- ( x e. A |-> B ) = ran ( x e. A |-> <. x , B >. )

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	|- B e. _V
2	1	dfmpt	|- ( x e. A |-> B ) = U_ x e. A { <. x , B >. }
3		eqid	|- ( x e. A |-> <. x , B >. ) = ( x e. A |-> <. x , B >. )
4	3	rnmpt	|- ran ( x e. A |-> <. x , B >. ) = { y | E. x e. A y = <. x , B >. }
5		velsn	|- ( y e. { <. x , B >. } <-> y = <. x , B >. )
6	5	rexbii	|- ( E. x e. A y e. { <. x , B >. } <-> E. x e. A y = <. x , B >. )
7	6	abbii	|- { y | E. x e. A y e. { <. x , B >. } } = { y | E. x e. A y = <. x , B >. }
8	4 7	eqtr4i	|- ran ( x e. A |-> <. x , B >. ) = { y | E. x e. A y e. { <. x , B >. } }
9		df-iun	|- U_ x e. A { <. x , B >. } = { y | E. x e. A y e. { <. x , B >. } }
10	8 9	eqtr4i	|- ran ( x e. A |-> <. x , B >. ) = U_ x e. A { <. x , B >. }
11	2 10	eqtr4i	|- ( x e. A |-> B ) = ran ( x e. A |-> <. x , B >. )