Theorem elrels5

Description: Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021)

	Ref	Expression
Assertion	elrels5	$$⊢R\in V\to \left(R\in \mathrm{Rels}\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrelsrel	$$⊢R\in V\to \left(R\in \mathrm{Rels}\leftrightarrow \mathrm{Rel}R\right)$$
2		dfrel5	$$⊢\mathrm{Rel}R\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R$$
3	1 2	bitrdi	$$⊢R\in V\to \left(R\in \mathrm{Rels}\leftrightarrow {R\upharpoonright }_{\mathrm{dom}R}=R\right)$$