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 )