Theorem cnvref5

Description: Two ways to say that a relation is a subclass of the identity relation. (Contributed by Peter Mazsa, 26-Jun-2019)

	Ref	Expression
Assertion	cnvref5	$$⊢\mathrm{Rel}R\to \left(R\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\left(xRy\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrel3	$$⊢\mathrm{Rel}R\to \left(R\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\left(xRy\to x\mathrm{I}y\right)\right)$$
2		ideqg	$$⊢y\in \mathrm{V}\to \left(x\mathrm{I}y\leftrightarrow x=y\right)$$
3	2	elv	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
4	3	imbi2i	$$⊢\left(xRy\to x\mathrm{I}y\right)\leftrightarrow \left(xRy\to x=y\right)$$
5	4	2albii	$$⊢\forall x\forall y\left(xRy\to x\mathrm{I}y\right)\leftrightarrow \forall x\forall y\left(xRy\to x=y\right)$$
6	1 5	bitrdi	$$⊢\mathrm{Rel}R\to \left(R\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\left(xRy\to x=y\right)\right)$$