Metamath Proof Explorer


Theorem dmqseq

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

Ref Expression
Assertion dmqseq R = S dom R / R = dom S / S

Proof

Step Hyp Ref Expression
1 dmeq R = S dom R = dom S
2 qseq12 dom R = dom S R = S dom R / R = dom S / S
3 1 2 mpancom R = S dom R / R = dom S / S