This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- F/_ x R
dfrel4.2 
|- F/_ y R
Assertion dfrel4 
|- ( Rel R <-> R = { <. x , y >. | x R y } )

Proof

Step Hyp Ref Expression
1 dfrel4.1 
 |-  F/_ x R
2 dfrel4.2 
 |-  F/_ y R
3 dfrel4v 
 |-  ( Rel R <-> R = { <. a , b >. | a R b } )
4 nfcv 
 |-  F/_ x a
5 nfcv 
 |-  F/_ x b
6 4 1 5 nfbr 
 |-  F/ x a R b
7 nfcv 
 |-  F/_ y a
8 nfcv 
 |-  F/_ y b
9 7 2 8 nfbr 
 |-  F/ y a R b
10 nfv 
 |-  F/ a x R y
11 nfv 
 |-  F/ b x R y
12 breq12 
 |-  ( ( a = x /\ b = y ) -> ( a R b <-> x R y ) )
13 6 9 10 11 12 cbvopab 
 |-  { <. a , b >. | a R b } = { <. x , y >. | x R y }
14 13 eqeq2i 
 |-  ( R = { <. a , b >. | a R b } <-> R = { <. x , y >. | x R y } )
15 3 14 bitri 
 |-  ( Rel R <-> R = { <. x , y >. | x R y } )