Metamath Proof Explorer

Theorem nelneq

Description: A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997)

Ref Expression
Assertion nelneq ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → ¬ 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
2 1 biimpcd ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 = 𝐵 → 𝐵 ∈ 𝐶 ) )
3 2 con3dimp ⊢ ( ( 𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶 ) → ¬ 𝐴 = 𝐵 )