Theorem elnelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020)

	Ref	Expression
Assertion	elnelne2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶 ) → 𝐴 ≠ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝐵 ∉ 𝐶 ↔ ¬ 𝐵 ∈ 𝐶 )
2		nelne2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → 𝐴 ≠ 𝐵 )
3	1 2	sylan2b	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶 ) → 𝐴 ≠ 𝐵 )