Metamath Proof Explorer

Theorem erALTVeq1

Description: Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021)

Ref Expression
Assertion erALTVeq1 
|- ( R = S -> ( R ErALTV A <-> S ErALTV A ) )

Proof

Step Hyp Ref Expression
1 eqvreleq 
 |-  ( R = S -> ( EqvRel R <-> EqvRel S ) )
2 dmqseqeq1 
 |-  ( R = S -> ( ( dom R /. R ) = A <-> ( dom S /. S ) = A ) )
3 1 2 anbi12d 
 |-  ( R = S -> ( ( EqvRel R /\ ( dom R /. R ) = A ) <-> ( EqvRel S /\ ( dom S /. S ) = A ) ) )
4 dferALTV2 
 |-  ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) )
5 dferALTV2 
 |-  ( S ErALTV A <-> ( EqvRel S /\ ( dom S /. S ) = A ) )
6 3 4 5 3bitr4g 
 |-  ( R = S -> ( R ErALTV A <-> S ErALTV A ) )