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	$$⊢\mathrm{Rel}R\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfrel2	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$
2		eqcom	$$⊢{R^{-1}}^{-1}=R\leftrightarrow R={R^{-1}}^{-1}$$
3		cnvcnv3	$$⊢{R^{-1}}^{-1}=\left\{⟨x,y⟩|xRy\right\}$$
4	3	eqeq2i	$$⊢R={R^{-1}}^{-1}\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$
5	1 2 4	3bitri	$$⊢\mathrm{Rel}R\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$