Metamath Proof Explorer


Theorem qseq12

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

Ref Expression
Assertion qseq12 A=BC=DA/C=B/D

Proof

Step Hyp Ref Expression
1 qseq1 A=BA/C=B/C
2 qseq2 C=DB/C=B/D
3 1 2 sylan9eq A=BC=DA/C=B/D