Metamath Proof Explorer

Theorem nelneq2

Description: A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002)

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

Proof

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