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

Metamath Proof Explorer

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