Theorem nelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

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

Proof

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