This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶 ) → 𝐴 ≠ 𝐵 )