Metamath Proof Explorer


Theorem dmqseqi

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

Ref Expression
Hypothesis dmqseqi.1 𝑅 = 𝑆
Assertion dmqseqi ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 )

Proof

Step Hyp Ref Expression
1 dmqseqi.1 𝑅 = 𝑆
2 dmqseq ( 𝑅 = 𝑆 → ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 ) )
3 1 2 ax-mp ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 )