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


Ref 
Expression 

Hypothesis 
difeq1i.1 
⊢ 𝐴 = 𝐵 

Assertion 
difeq1i 
⊢ ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

difeq1i.1 
⊢ 𝐴 = 𝐵 
2 

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

axmp 
⊢ ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐶 ) 