This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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