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 | φ ran R = y | x φ

Proof

Step Hyp Ref Expression
1 dfrn2 ran R = y | x x R y
2 nfopab2 _ y x y | φ
3 2 nfeq2 y R = x y | φ
4 nfopab1 _ x x y | φ
5 4 nfeq2 x R = x y | φ
6 df-br x R y x y R
7 eleq2 R = x y | φ x y R x y x y | φ
8 opabidw x y x y | φ φ
9 7 8 bitrdi R = x y | φ x y R φ
10 6 9 syl5bb R = x y | φ x R y φ
11 5 10 exbid R = x y | φ x x R y x φ
12 3 11 abbid R = x y | φ y | x x R y = y | x φ
13 1 12 syl5eq R = x y | φ ran R = y | x φ