Theorem dfrel4v

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)

	Ref	Expression
Assertion	dfrel4v	|- ( Rel R <-> R = { <. x , y >. | x R y } )

Proof

Step	Hyp	Ref	Expression
1		dfrel2	|- ( Rel R <-> `' `' R = R )
2		eqcom	|- ( `' `' R = R <-> R = `' `' R )
3		cnvcnv3	|- `' `' R = { <. x , y >. | x R y }
4	3	eqeq2i	|- ( R = `' `' R <-> R = { <. x , y >. | x R y } )
5	1 2 4	3bitri	|- ( Rel R <-> R = { <. x , y >. | x R y } )