Metamath Proof Explorer

Theorem dfeqvrel3

Description: Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019)

		Ref	Expression
	Assertion	dfeqvrel3	$⊢ EqvRel 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)) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$
2		refsymrel3	$⊢ (RefRel R \land SymRel R) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R)$
3		dftrrel3	$⊢ TrRel R \leftrightarrow (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R)$
4	2 3	anbi12i	$⊢ ((RefRel R \land SymRel R) \land TrRel R) \leftrightarrow (((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R) \land (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R))$
5		df-3an	$⊢ (RefRel R \land SymRel R \land TrRel R) \leftrightarrow ((RefRel R \land SymRel R) \land TrRel R)$
6		df-3an	$⊢ (\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)) \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))$
7	6	anbi1i	$⊢ ((\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)) \land Rel 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)) \land Rel R)$
8		3anan32	$⊢ ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \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)) \land Rel R)$
9		anandi3r	$⊢ ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \leftrightarrow (((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R) \land (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R))$
10	7 8 9	3bitr2i	$⊢ ((\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)) \land Rel R) \leftrightarrow (((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land Rel R) \land (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \land Rel R))$
11	4 5 10	3bitr4i	$⊢ (RefRel R \land SymRel R \land TrRel 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)) \land Rel R)$
12	1 11	bitri	$⊢ EqvRel 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)) \land Rel R)$