Metamath Proof Explorer

Theorem eleqvrelsrel

Description: For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate. (Contributed by Peter Mazsa, 24-Aug-2021)

		Ref	Expression
	Assertion	eleqvrelsrel	$⊢ R \in V \to (R \in EqvRels \leftrightarrow EqvRel R)$

Proof

Step	Hyp	Ref	Expression
1		elrelsrel	$⊢ R \in V \to (R \in Rels \leftrightarrow Rel R)$
2	1	anbi2d	$⊢ R \in V \to ((({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land R \in Rels) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R))$
3		eleqvrels2	$⊢ R \in EqvRels \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land R \in Rels)$
4		dfeqvrel2	$⊢ EqvRel R \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R \land R \circ R \subseteq R) \land Rel R)$
5	2 3 4	3bitr4g	$⊢ R \in V \to (R \in EqvRels \leftrightarrow EqvRel R)$