Metamath Proof Explorer


Theorem dmqseq

Description: Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Assertion dmqseq ( 𝑅 = 𝑆 → ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 ) )

Proof

Step Hyp Ref Expression
1 dmeq ( 𝑅 = 𝑆 → dom 𝑅 = dom 𝑆 )
2 qseq12 ( ( dom 𝑅 = dom 𝑆𝑅 = 𝑆 ) → ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 ) )
3 1 2 mpancom ( 𝑅 = 𝑆 → ( dom 𝑅 / 𝑅 ) = ( dom 𝑆 / 𝑆 ) )