Theorem nelneq2 2713

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

Assertion

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

Proof of Theorem nelneq2

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  ssnelpss  3680  opthwiener  4901  ssfin4  9015  pwxpndom2  9366  fzneuz  12290  hauspwpwf1  21601  vdgr1b  26431  topdifinffinlem  32371  clsk1indlem1  37363