This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )