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

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 ⊢ 𝑅 = 𝑆
Assertion erALTVeq1i ( 𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴 )

Proof

Step Hyp Ref Expression
1 erALTVeq1i.1 ⊢ 𝑅 = 𝑆
2 erALTVeq1 ⊢ ( 𝑅 = 𝑆 → ( 𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴 ) )
3 1 2 ax-mp ⊢ ( 𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴 )