Theorem elrels6

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

	Ref	Expression
Assertion	elrels6	$$⊢R\in V\to \left(R\in \mathrm{Rels}\leftrightarrow R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)=R\right)$$

Proof

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