Theorem nelne2 3057

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2839  df-ne 2960

This theorem is used by:  nelelne  3060  elnelne2  3077  elneeldif  4056  elpwdifsn  4752  f1ounsn  7290  ac5num  10128  infpssrlem4  10397  fpwwe2lem12  10740  zgt1rpn0n1  13176  cats1un  14884  dprdfadd  20251  dprdcntz2  20269  lbsextlem4  21454  lindff1  22141  hauscmplem  23739  fileln0  24184  zcld  25148  dvcnvlem  26311  ppinprm  27494  chtnprm  27496  tglnpt4  29138  footexALT  29208  footexlem1  29209  footexlem2  29210  foot  29212  colperpexlem3  29223  mideulem2  29225  opphllem  29226  opphllem2  29239  lnopp2hpgb  29256  colhp  29263  plngrotlem1  29280  plngrotlem2  29281  plngrot  29283  lnssplnglem  29284  lmieu  29304  trgcopy  29326  trgcopyeulem  29327  ragraghl  29361  tgaaddcpbllem1  29364  tgaaddcpbl  29367  perpprlng  29443  prlngex  29444  prlngmolem1  29445  prlngmid2  29454  quadcgrprlng  29459  tgextahpl  33084  tgextalem1inag  33085  cycpmco2lem1  33743  cycpmco2  33750  cyc3genpmlem  33768  unitnz  33855  fracfld  33926  linds2eq  33992  elrspunsn  34035  mxidlnzr  34048  lindsunlem  34312  fedgmul  34319  extdg1id  34354  2sqr3minply  34468  cos9thpiminplylem2  34471  ordtconnlem1  34612  esum2dlem  34780  subfacp1lem5  36073  heiborlem6  38896  llnle  40721  lplnle  40743  lhpexle1lem  41210  cdleme18b  41495  cdlemg46  41938  cdlemh  42020  ine1  43517  bcc0  45470  fnchoice  46191  climxrre  46905  stoweidlem43  47198  zneoALTV  48912  oppfrcllem  50388  oppfrcl2  50390  eloppf  50394