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	$⊢ Rel R \to (R \subseteq I \leftrightarrow \forall x \forall y (x R y \to x = y))$

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

Metamath Proof Explorer