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 ≀ 𝑅 ↔ TrRel ≀ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	⊢ ( EqvRel ≀ 𝑅 ↔ ( RefRel ≀ 𝑅 ∧ SymRel ≀ 𝑅 ∧ TrRel ≀ 𝑅 ) )
2		refrelcoss	⊢ RefRel ≀ 𝑅
3		symrelcoss	⊢ SymRel ≀ 𝑅
4	2 3	triantru3	⊢ ( TrRel ≀ 𝑅 ↔ ( RefRel ≀ 𝑅 ∧ SymRel ≀ 𝑅 ∧ TrRel ≀ 𝑅 ) )
5	1 4	bitr4i	⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅 )