Theorem nelne1

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

	Ref	Expression
Assertion	nelne1	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → 𝐵 ≠ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		nelneq2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → ¬ 𝐵 = 𝐶 )
2	1	neqned	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → 𝐵 ≠ 𝐶 )