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 <-> TrRel ,~ R )

Proof

Step Hyp Ref Expression
1 df-eqvrel 
 |-  ( EqvRel ,~ R <-> ( RefRel ,~ R /\ SymRel ,~ R /\ TrRel ,~ R ) )
2 refrelcoss 
 |-  RefRel ,~ R
3 symrelcoss 
 |-  SymRel ,~ R
4 2 3 triantru3 
 |-  ( TrRel ,~ R <-> ( RefRel ,~ R /\ SymRel ,~ R /\ TrRel ,~ R ) )
5 1 4 bitr4i 
 |-  ( EqvRel ,~ R <-> TrRel ,~ R )