Theorem nelne2 3042

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)

Assertion

Ref	Expression
nelne2	⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Proof of Theorem nelne2

Step	Hyp	Ref	Expression
1		nelneq 2863	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2950	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-ne 2944

This theorem is referenced by:  nelelne  3043  elnelne2  3060  elneeldif  3901  elpwdifsn  4722  ac5num  9792  infpssrlem4  10062  fpwwe2lem12  10398  zgt1rpn0n1  12771  cats1un  14434  dprdfadd  19623  dprdcntz2  19641  lbsextlem4  20423  lindff1  21027  hauscmplem  22557  fileln0  23001  zcld  23976  dvcnvlem  25140  ppinprm  26301  chtnprm  26303  footexALT  27079  footexlem1  27080  footexlem2  27081  foot  27083  colperpexlem3  27093  mideulem2  27095  opphllem  27096  opphllem2  27109  lnopp2hpgb  27124  colhp  27131  lmieu  27145  trgcopy  27165  trgcopyeulem  27166  cycpmco2lem1  31393  cycpmco2  31400  cyc3genpmlem  31418  linds2eq  31575  mxidlnzr  31639  lindsunlem  31705  fedgmul  31712  extdg1id  31738  ordtconnlem1  31874  esum2dlem  32060  subfacp1lem5  33146  heiborlem6  35974  llnle  37532  lplnle  37554  lhpexle1lem  38021  cdleme18b  38306  cdlemg46  38749  cdlemh  38831  bcc0  41958  fnchoice  42572  climxrre  43291  stoweidlem43  43584  zneoALTV  45121