Metamath Proof Explorer

Theorem erALTVeq1i

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

Ref Expression
Hypothesis erALTVeq1i.1 
|- R = S
Assertion erALTVeq1i 
|- ( R ErALTV A <-> S ErALTV A )

Proof

Step Hyp Ref Expression
1 erALTVeq1i.1 
 |-  R = S
2 erALTVeq1 
 |-  ( R = S -> ( R ErALTV A <-> S ErALTV A ) )
3 1 2 ax-mp 
 |-  ( R ErALTV A <-> S ErALTV A )