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