Theorem dfrel5

Description: Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 6-Nov-2018)

	Ref	Expression
Assertion	dfrel5	$$⊢\mathrm{Rel}R\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R$$

Proof

Step	Hyp	Ref	Expression
1		dfrel2	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$
2		resdm2	$$⊢{R\upharpoonright }_{\mathrm{dom}R}={R^{-1}}^{-1}$$
3	2	eqeq1i	$$⊢{R\upharpoonright }_{\mathrm{dom}R}=R\leftrightarrow {R^{-1}}^{-1}=R$$
4	1 3	bitr4i	$$⊢\mathrm{Rel}R\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R$$