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

Metamath Proof Explorer

Theorem imaopab

Description: The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023)

Ref Expression
Assertion imaopab 
|- ( { <. x , y >. | ph } " A ) = { y | E. x e. A ph }

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( { <. x , y >. | ph } " A ) = ran ( { <. x , y >. | ph } |` A )
2 resopab 
 |-  ( { <. x , y >. | ph } |` A ) = { <. x , y >. | ( x e. A /\ ph ) }
3 2 rneqi 
 |-  ran ( { <. x , y >. | ph } |` A ) = ran { <. x , y >. | ( x e. A /\ ph ) }
4 rnopab 
 |-  ran { <. x , y >. | ( x e. A /\ ph ) } = { y | E. x ( x e. A /\ ph ) }
5 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
6 5 abbii 
 |-  { y | E. x e. A ph } = { y | E. x ( x e. A /\ ph ) }
7 4 6 eqtr4i 
 |-  ran { <. x , y >. | ( x e. A /\ ph ) } = { y | E. x e. A ph }
8 1 3 7 3eqtri 
 |-  ( { <. x , y >. | ph } " A ) = { y | E. x e. A ph }