Metamath Proof Explorer

Theorem opabrn

Description: Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Assertion opabrn 
|- ( R = { <. x , y >. | ph } -> ran R = { y | E. x ph } )

Proof

Step Hyp Ref Expression
1 dfrn2 
 |-  ran R = { y | E. x x R y }
2 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
3 2 nfeq2 
 |-  F/ y R = { <. x , y >. | ph }
4 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
5 4 nfeq2 
 |-  F/ x R = { <. x , y >. | ph }
6 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
7 eleq2 
 |-  ( R = { <. x , y >. | ph } -> ( <. x , y >. e. R <-> <. x , y >. e. { <. x , y >. | ph } ) )
8 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
9 7 8 bitrdi 
 |-  ( R = { <. x , y >. | ph } -> ( <. x , y >. e. R <-> ph ) )
10 6 9 syl5bb 
 |-  ( R = { <. x , y >. | ph } -> ( x R y <-> ph ) )
11 5 10 exbid 
 |-  ( R = { <. x , y >. | ph } -> ( E. x x R y <-> E. x ph ) )
12 3 11 abbid 
 |-  ( R = { <. x , y >. | ph } -> { y | E. x x R y } = { y | E. x ph } )
13 1 12 syl5eq 
 |-  ( R = { <. x , y >. | ph } -> ran R = { y | E. x ph } )