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	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	eldifd.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐶 )
Assertion	eldifd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		eldifd.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐶 )
3		eldif	⊢ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) )
4	1 2 3	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) )