Metamath Proof Explorer

Theorem dfeqvrel2

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

		Ref	Expression
	Assertion	dfeqvrel2	$⊢ EqvRel R \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$
2		refsymrel2	$⊢ (RefRel R \land SymRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R)$
3		dftrrel2	$⊢ TrRel R \leftrightarrow (R \circ R \subseteq R \land Rel R)$
4	2 3	anbi12i	$⊢ ((RefRel R \land SymRel R) \land TrRel R) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R) \land (R \circ R \subseteq R \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	$⊢ ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \circ R \subseteq R)$
7	6	anbi1i	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \circ R \subseteq R) \land Rel R)$
8		3anan32	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R \land R \circ R \subseteq R) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \circ R \subseteq R) \land Rel R)$
9		anandi3r	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R \land R \circ R \subseteq R) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R) \land (R \circ R \subseteq R \land Rel R))$
10	7 8 9	3bitr2i	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R) \leftrightarrow ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land Rel R) \land (R \circ R \subseteq R \land Rel R))$
11	4 5 10	3bitr4i	$⊢ (RefRel R \land SymRel R \land TrRel R) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$
12	1 11	bitri	$⊢ EqvRel R \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$