Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The difference of two classes
difss2d
Metamath Proof Explorer
Description: If a class is contained in a difference, it is contained in the minuend.
Deduction form of difss2 . (Contributed by David Moews , 1-May-2017)

Ref
Expression
Hypothesis
difss2d.1
$${\u22a2}{\phi}\to {A}\subseteq {B}\setminus {C}$$
Assertion
difss2d
$${\u22a2}{\phi}\to {A}\subseteq {B}$$

Proof
Step
Hyp
Ref
Expression
1
difss2d.1
$${\u22a2}{\phi}\to {A}\subseteq {B}\setminus {C}$$
2
difss2
$${\u22a2}{A}\subseteq {B}\setminus {C}\to {A}\subseteq {B}$$
3
1 2
syl
$${\u22a2}{\phi}\to {A}\subseteq {B}$$