Theorem dfrel6

Description: Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019)

	Ref	Expression
Assertion	dfrel6	$$⊢\mathrm{Rel}R\leftrightarrow R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		dfrel5	$$⊢\mathrm{Rel}R\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R$$
2		dfres3	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
3	2	eqeq1i	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\leftrightarrow R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)=R$$
4	1 3	bitri	$$⊢\mathrm{Rel}R\leftrightarrow R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)=R$$