Theorem imadmrn

Description: The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994)

	Ref	Expression
Assertion	imadmrn	|- ( A " dom A ) = ran A

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		vex	|- y e. _V
3	1 2	opeldm	|- ( <. x , y >. e. A -> x e. dom A )
4	3	pm4.71i	|- ( <. x , y >. e. A <-> ( <. x , y >. e. A /\ x e. dom A ) )
5		ancom	|- ( ( <. x , y >. e. A /\ x e. dom A ) <-> ( x e. dom A /\ <. x , y >. e. A ) )
6	4 5	bitr2i	|- ( ( x e. dom A /\ <. x , y >. e. A ) <-> <. x , y >. e. A )
7	6	exbii	|- ( E. x ( x e. dom A /\ <. x , y >. e. A ) <-> E. x <. x , y >. e. A )
8	7	abbii	|- { y | E. x ( x e. dom A /\ <. x , y >. e. A ) } = { y | E. x <. x , y >. e. A }
9		dfima3	|- ( A " dom A ) = { y | E. x ( x e. dom A /\ <. x , y >. e. A ) }
10		dfrn3	|- ran A = { y | E. x <. x , y >. e. A }
11	8 9 10	3eqtr4i	|- ( A " dom A ) = ran A