Metamath Proof Explorer

Theorem eqvrelcoss

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020) (Revised by Peter Mazsa, 20-Dec-2021)

		Ref	Expression
	Assertion	eqvrelcoss	$⊢ EqvRel ≀ R \leftrightarrow TrRel ≀ R$

Step	Hyp	Ref	Expression
1		df-eqvrel	$⊢ EqvRel ≀ R \leftrightarrow (RefRel ≀ R \land SymRel ≀ R \land TrRel ≀ R)$
2		refrelcoss	$⊢ RefRel ≀ R$
3		symrelcoss	$⊢ SymRel ≀ R$
4	2 3	triantru3	$⊢ TrRel ≀ R \leftrightarrow (RefRel ≀ R \land SymRel ≀ R \land TrRel ≀ R)$
5	1 4	bitr4i	$⊢ EqvRel ≀ R \leftrightarrow TrRel ≀ R$