Theorem dmqseqeq1i

Description: Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Hypothesis	dmqseqeq1i.1	⊢ 𝑅 = 𝑆
Assertion	dmqseqeq1i	⊢ ( ( dom 𝑅 / 𝑅 ) = 𝐴 ↔ ( dom 𝑆 / 𝑆 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dmqseqeq1i.1	⊢ 𝑅 = 𝑆
2		dmqseqeq1	⊢ ( 𝑅 = 𝑆 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 ↔ ( dom 𝑆 / 𝑆 ) = 𝐴 ) )
3	1 2	ax-mp	⊢ ( ( dom 𝑅 / 𝑅 ) = 𝐴 ↔ ( dom 𝑆 / 𝑆 ) = 𝐴 )