Metamath Proof Explorer
Description: Inference adding difference to the right in a class equality.
(Contributed by NM, 15Nov2002)


Ref 
Expression 

Hypothesis 
difeq1i.1 
$${\u22a2}{A}={B}$$ 

Assertion 
difeq1i 
$${\u22a2}{A}\setminus {C}={B}\setminus {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

difeq1i.1 
$${\u22a2}{A}={B}$$ 
2 

difeq1 
$${\u22a2}{A}={B}\to {A}\setminus {C}={B}\setminus {C}$$ 
3 
1 2

axmp 
$${\u22a2}{A}\setminus {C}={B}\setminus {C}$$ 