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


Ref 
Expression 

Hypothesis 
difeq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 

Assertion 
difeq2d 
⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

difeq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 
2 

difeq2 
⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) 
3 
1 2

syl 
⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) 