Metamath Proof Explorer
Description: A difference of two classes is contained in the minuend. Deduction form
of difss . (Contributed by David Moews, 1May2017)


Ref 
Expression 

Assertion 
difssd 
$${\u22a2}{\phi}\to {A}\setminus {B}\subseteq {A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

difss 
$${\u22a2}{A}\setminus {B}\subseteq {A}$$ 
2 
1

a1i 
$${\u22a2}{\phi}\to {A}\setminus {B}\subseteq {A}$$ 