Theorem rnopab3

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

	Ref	Expression
Assertion	rnopab3	|- ( A. y e. A E. x ph <-> ran { <. x , y >. | ( y e. A /\ ph ) } = A )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. y e. A E. x ph <-> A. y ( y e. A -> E. x ph ) )
2		pm4.71	|- ( ( y e. A -> E. x ph ) <-> ( y e. A <-> ( y e. A /\ E. x ph ) ) )
3	2	albii	|- ( A. y ( y e. A -> E. x ph ) <-> A. y ( y e. A <-> ( y e. A /\ E. x ph ) ) )
4		rnopab	|- ran { <. x , y >. | ( y e. A /\ ph ) } = { y | E. x ( y e. A /\ ph ) }
5		19.42v	|- ( E. x ( y e. A /\ ph ) <-> ( y e. A /\ E. x ph ) )
6	5	abbii	|- { y | E. x ( y e. A /\ ph ) } = { y | ( y e. A /\ E. x ph ) }
7	4 6	eqtri	|- ran { <. x , y >. | ( y e. A /\ ph ) } = { y | ( y e. A /\ E. x ph ) }
8	7	eqeq1i	|- ( ran { <. x , y >. | ( y e. A /\ ph ) } = A <-> { y | ( y e. A /\ E. x ph ) } = A )
9		eqcom	|- ( A = { y | ( y e. A /\ E. x ph ) } <-> { y | ( y e. A /\ E. x ph ) } = A )
10		eqabb	|- ( A = { y | ( y e. A /\ E. x ph ) } <-> A. y ( y e. A <-> ( y e. A /\ E. x ph ) ) )
11	8 9 10	3bitr2ri	|- ( A. y ( y e. A <-> ( y e. A /\ E. x ph ) ) <-> ran { <. x , y >. | ( y e. A /\ ph ) } = A )
12	1 3 11	3bitri	|- ( A. y e. A E. x ph <-> ran { <. x , y >. | ( y e. A /\ ph ) } = A )