Metamath Proof Explorer


Theorem difeq12

Description: Equality theorem for class difference. (Contributed by FL, 31-Aug-2009)

Ref Expression
Assertion difeq12 ⊢ A = B ∧ C = D → A ∖ C = B ∖ D

Proof

Step Hyp Ref Expression
1 difeq1 ⊢ A = B → A ∖ C = B ∖ C
2 difeq2 ⊢ C = D → B ∖ C = B ∖ D
3 1 2 sylan9eq ⊢ A = B ∧ C = D → A ∖ C = B ∖ D