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

Metamath Proof Explorer

Theorem rnopab

Description: The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995) (Revised by Mario Carneiro, 4-Dec-2016)

Ref Expression
Assertion rnopab 
|- ran { <. x , y >. | ph } = { y | E. x ph }

Proof

Step Hyp Ref Expression
1 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
2 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
3 1 2 dfrnf 
 |-  ran { <. x , y >. | ph } = { y | E. x x { <. x , y >. | ph } y }
4 df-br 
 |-  ( x { <. x , y >. | ph } y <-> <. x , y >. e. { <. x , y >. | ph } )
5 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
6 4 5 bitri 
 |-  ( x { <. x , y >. | ph } y <-> ph )
7 6 exbii 
 |-  ( E. x x { <. x , y >. | ph } y <-> E. x ph )
8 7 abbii 
 |-  { y | E. x x { <. x , y >. | ph } y } = { y | E. x ph }
9 3 8 eqtri 
 |-  ran { <. x , y >. | ph } = { y | E. x ph }