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