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	|- ran { <. x , y >. | ( y e. A /\ ph ) } C_ A

Proof

Step	Hyp	Ref	Expression
1		rnopab	|- ran { <. x , y >. | ( y e. A /\ ph ) } = { y | E. x ( y e. A /\ ph ) }
2		19.42v	|- ( E. x ( y e. A /\ ph ) <-> ( y e. A /\ E. x ph ) )
3	2	abbii	|- { y | E. x ( y e. A /\ ph ) } = { y | ( y e. A /\ E. x ph ) }
4		ssab2	|- { y | ( y e. A /\ E. x ph ) } C_ A
5	3 4	eqsstri	|- { y | E. x ( y e. A /\ ph ) } C_ A
6	1 5	eqsstri	|- ran { <. x , y >. | ( y e. A /\ ph ) } C_ A