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 } )