Theorem nelne2 3062

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 2893	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2971	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-ne 2965

This theorem is referenced by:  nelelne  3065  elnelne2  3082  elneeldif  3927  elpwdifsn  4761  f1ounsn  7271  ac5num  10020  infpssrlem4  10290  fpwwe2lem12  10627  zgt1rpn0n1  13059  cats1un  14758  dprdfadd  20092  dprdcntz2  20110  lbsextlem4  21263  lindff1  21939  hauscmplem  23532  fileln0  23976  zcld  24940  dvcnvlem  26104  ppinprm  27282  chtnprm  27284  tglnpt4  28890  footexALT  28957  footexlem1  28958  footexlem2  28959  foot  28961  colperpexlem3  28972  mideulem2  28974  opphllem  28975  opphllem2  28988  lnopp2hpgb  29004  colhp  29011  plngrotlem1  29027  plngrotlem2  29028  plngrot  29030  lnssplnglem  29031  lmieu  29051  trgcopy  29072  trgcopyeulem  29073  ragraghl  29104  perpprlng  29153  prlngex  29154  prlngmolem1  29155  cycpmco2lem1  33387  cycpmco2  33394  cyc3genpmlem  33412  unitnz  33499  fracfld  33572  linds2eq  33638  elrspunsn  33681  mxidlnzr  33695  lindsunlem  33959  fedgmul  33966  extdg1id  34001  2sqr3minply  34115  cos9thpiminplylem2  34118  ordtconnlem1  34259  esum2dlem  34427  subfacp1lem5  35609  mh-inf3f1  36975  heiborlem6  38389  llnle  40216  lplnle  40238  lhpexle1lem  40705  cdleme18b  40990  cdlemg46  41433  cdlemh  41515  ine1  42999  bcc0  44976  fnchoice  45675  climxrre  46390  stoweidlem43  46683  zneoALTV  48357  oppfrcllem  49824  oppfrcl2  49826  eloppf  49830