Theorem dmqseqd

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

	Ref	Expression
Hypothesis	dmqseqd.1	$$⊢\phi \to R=S$$
Assertion	dmqseqd	$$⊢\phi \to \mathrm{dom}R/R=\mathrm{dom}S/S$$

Proof

Step	Hyp	Ref	Expression
1		dmqseqd.1	$$⊢\phi \to R=S$$
2		dmqseq	$$⊢R=S\to \mathrm{dom}R/R=\mathrm{dom}S/S$$
3	1 2	syl	$$⊢\phi \to \mathrm{dom}R/R=\mathrm{dom}S/S$$