dfeqvrels3

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

		Ref	Expression
	Assertion	dfeqvrels3	$⊢ EqvRels = \{r \in Rels \| (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x) \land \forall x \forall y \forall z ((x r y \land y r z) \to x r z))\}$

Step	Hyp	Ref	Expression
1		dfeqvrels2	$⊢ EqvRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r)\}$
2		idrefALT	$⊢ {I ↾}_{dom r} \subseteq r \leftrightarrow \forall x \in dom r x r x$
3		cnvsym	$⊢ r^{-1} \subseteq r \leftrightarrow \forall x \forall y (x r y \to y r x)$
4		cotr	$⊢ r \circ r \subseteq r \leftrightarrow \forall x \forall y \forall z ((x r y \land y r z) \to x r z)$
5	2 3 4	3anbi123i	$⊢ ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r \land r \circ r \subseteq r) \leftrightarrow (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x) \land \forall x \forall y \forall z ((x r y \land y r z) \to x r z))$
6	1 5	rabbieq	$⊢ EqvRels = \{r \in Rels \| (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x) \land \forall x \forall y \forall z ((x r y \land y r z) \to x r z))\}$

Metamath Proof Explorer