Metamath Proof Explorer

Theorem eqvreleq

Description: Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 23-Sep-2021)

Ref Expression
Assertion eqvreleq 
|- ( R = S -> ( EqvRel R <-> EqvRel S ) )

Proof

Step Hyp Ref Expression
1 refreleq 
 |-  ( R = S -> ( RefRel R <-> RefRel S ) )
2 symreleq 
 |-  ( R = S -> ( SymRel R <-> SymRel S ) )
3 trreleq 
 |-  ( R = S -> ( TrRel R <-> TrRel S ) )
4 1 2 3 3anbi123d 
 |-  ( R = S -> ( ( RefRel R /\ SymRel R /\ TrRel R ) <-> ( RefRel S /\ SymRel S /\ TrRel S ) ) )
5 df-eqvrel 
 |-  ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )
6 df-eqvrel 
 |-  ( EqvRel S <-> ( RefRel S /\ SymRel S /\ TrRel S ) )
7 4 5 6 3bitr4g 
 |-  ( R = S -> ( EqvRel R <-> EqvRel S ) )