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 }