Theorem rnopabss

Description: Upper bound for the range of a restricted class of ordered pairs. (Contributed by Eric Schmidt, 16-Sep-2025)

	Ref	Expression
Assertion	rnopabss	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(y\in A\wedge \phi \right)\right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(y\in A\wedge \phi \right)\right\}=\left\{y|\exists x\left(y\in A\wedge \phi \right)\right\}$$
2		19.42v	$$⊢\exists x\left(y\in A\wedge \phi \right)\leftrightarrow \left(y\in A\wedge \exists x\phi \right)$$
3	2	abbii	$$⊢\left\{y|\exists x\left(y\in A\wedge \phi \right)\right\}=\left\{y|\left(y\in A\wedge \exists x\phi \right)\right\}$$
4		ssab2	$$⊢\left\{y|\left(y\in A\wedge \exists x\phi \right)\right\}\subseteq A$$
5	3 4	eqsstri	$$⊢\left\{y|\exists x\left(y\in A\wedge \phi \right)\right\}\subseteq A$$
6	1 5	eqsstri	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(y\in A\wedge \phi \right)\right\}\subseteq A$$