Metamath Proof Explorer


Theorem qseq12

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

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

Proof

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