Metamath Proof Explorer


Theorem qseq12

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

Ref Expression
Assertion qseq12 ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐷 ) )

Proof

Step Hyp Ref Expression
1 qseq1 ( 𝐴 = 𝐵 → ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐶 ) )
2 qseq2 ( 𝐶 = 𝐷 → ( 𝐵 / 𝐶 ) = ( 𝐵 / 𝐷 ) )
3 1 2 sylan9eq ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐷 ) )