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	|- ( ph -> A e. B )
	eldifd.2	|- ( ph -> -. A e. C )
Assertion	eldifd	|- ( ph -> A e. ( B \ C ) )

Proof

Step	Hyp	Ref	Expression
1		eldifd.1	|- ( ph -> A e. B )
2		eldifd.2	|- ( ph -> -. A e. C )
3		eldif	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
4	1 2 3	sylanbrc	|- ( ph -> A e. ( B \ C ) )