This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difeq12i

Description: Equality inference for class difference. (Contributed by NM, 29-Aug-2004)

Ref Expression
Hypotheses difeq1i.1 ⊢ A = B
difeq12i.2 ⊢ C = D
Assertion difeq12i ⊢ A ∖ C = B ∖ D

Proof

Step Hyp Ref Expression
1 difeq1i.1 ⊢ A = B
2 difeq12i.2 ⊢ C = D
3 1 difeq1i ⊢ A ∖ C = B ∖ C
4 2 difeq2i ⊢ B ∖ C = B ∖ D
5 3 4 eqtri ⊢ A ∖ C = B ∖ D