Theorem eldifd

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	eldifd.1	$$⊢\phi \to A\in B$$
	eldifd.2	$$⊢\phi \to \neg A\in C$$
Assertion	eldifd	$$⊢\phi \to A\in \left(B\setminus C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldifd.1	$$⊢\phi \to A\in B$$
2		eldifd.2	$$⊢\phi \to \neg A\in C$$
3		eldif	$$⊢A\in \left(B\setminus C\right)\leftrightarrow \left(A\in B\wedge \neg A\in C\right)$$
4	1 2 3	sylanbrc	$$⊢\phi \to A\in \left(B\setminus C\right)$$