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=xy|φranR=y|xφ

Proof

Step Hyp Ref Expression
1 dfrn2 ranR=y|xxRy
2 nfopab2 _yxy|φ
3 2 nfeq2 yR=xy|φ
4 nfopab1 _xxy|φ
5 4 nfeq2 xR=xy|φ
6 df-br xRyxyR
7 eleq2 R=xy|φxyRxyxy|φ
8 opabidw xyxy|φφ
9 7 8 bitrdi R=xy|φxyRφ
10 6 9 syl5bb R=xy|φxRyφ
11 5 10 exbid R=xy|φxxRyxφ
12 3 11 abbid R=xy|φy|xxRy=y|xφ
13 1 12 eqtrid R=xy|φranR=y|xφ