Theorem elndif

Description: A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994)

	Ref	Expression
Assertion	elndif	⊢ ( 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifn	⊢ ( 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) → ¬ 𝐴 ∈ 𝐵 )
2	1	con2i	⊢ ( 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ ( 𝐶 ∖ 𝐵 ) )