Metamath Proof Explorer


Theorem dmqseqd

Description: Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021)

Ref Expression
Hypothesis dmqseqd.1 φ R = S
Assertion dmqseqd φ dom R / R = dom S / S

Proof

Step Hyp Ref Expression
1 dmqseqd.1 φ R = S
2 dmqseq R = S dom R / R = dom S / S
3 1 2 syl φ dom R / R = dom S / S