Metamath Proof Explorer


Theorem dfrel4

Description: A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 for relations. (Contributed by Mario Carneiro, 16-Aug-2015) (Revised by Thierry Arnoux, 11-May-2017)

Ref Expression
Hypotheses dfrel4.1 _xR
dfrel4.2 _yR
Assertion dfrel4 RelRR=xy|xRy

Proof

Step Hyp Ref Expression
1 dfrel4.1 _xR
2 dfrel4.2 _yR
3 dfrel4v RelRR=ab|aRb
4 nfcv _xa
5 nfcv _xb
6 4 1 5 nfbr xaRb
7 nfcv _ya
8 nfcv _yb
9 7 2 8 nfbr yaRb
10 nfv axRy
11 nfv bxRy
12 breq12 a=xb=yaRbxRy
13 6 9 10 11 12 cbvopab ab|aRb=xy|xRy
14 13 eqeq2i R=ab|aRbR=xy|xRy
15 3 14 bitri RelRR=xy|xRy