Theorem imaopab

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

	Ref	Expression
Assertion	imaopab	$$⊢\left\{⟨x,y⟩|\phi \right\}\left[A\right]=\left\{y|\exists x\in A\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢\left\{⟨x,y⟩|\phi \right\}\left[A\right]=\mathrm{ran}\left({\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A\right)$$
2		resopab	$$⊢{\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
3	2	rneqi	$$⊢\mathrm{ran}\left({\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A\right)=\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$
4		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\exists x\left(x\in A\wedge \phi \right)\right\}$$
5		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
6	5	abbii	$$⊢\left\{y|\exists x\in A\phi \right\}=\left\{y|\exists x\left(x\in A\wedge \phi \right)\right\}$$
7	4 6	eqtr4i	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=\left\{y|\exists x\in A\phi \right\}$$
8	1 3 7	3eqtri	$$⊢\left\{⟨x,y⟩|\phi \right\}\left[A\right]=\left\{y|\exists x\in A\phi \right\}$$