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 R = S
Assertion dmqseqi dom R / R = dom S / S

Proof

Step Hyp Ref Expression
1 dmqseqi.1 R = S
2 dmqseq R = S dom R / R = dom S / S
3 1 2 ax-mp dom R / R = dom S / S