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

Metamath Proof Explorer

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 >. )