MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq1 Unicode version

Theorem neeq1 2738
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq1

Proof of Theorem neeq1
StepHypRef Expression
1 id 22 . 2
21neeq1d 2734 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652
This theorem is referenced by:  neeq1iOLD  2743  neeq1dOLD  2748  nelrdva  3309  psseq1  3590  0inp0  4624  nnullss  4714  opeqex  4743  fri  4846  limeq  4895  xp11  5447  tz6.12i  5891  fveqressseq  6027  fprg  6080  f1dom3el3dif  6176  isofrlem  6236  f1oweALT  6784  frxp  6910  suppimacnv  6929  elqsn0  7399  frfi  7785  fiint  7817  marypha1lem  7913  dfac8alem  8431  dfac8clem  8434  aceq3lem  8522  dfac5lem3  8527  dfac5lem4  8528  dfac5  8530  dfac2  8532  dfac9  8537  kmlem1  8551  kmlem12  8562  kmlem14  8564  fin2i  8696  isfin2-2  8720  fin23lem21  8740  fin1a2lem10  8810  axcc2lem  8837  dominf  8846  ac5b  8879  zornn0g  8906  axdclem  8920  dominfac  8969  elwina  9085  elina  9086  iswun  9103  rankcf  9176  axrrecex  9561  elimne0  9607  1re  9616  recex  10206  uzn0  11125  qreccl  11231  xrnemnf  11357  xrnepnf  11358  fztpval  11770  expcl2lem  12178  hashnemnf  12417  hashneq0  12434  ntrivcvgn0  13707  ntrivcvgmullem  13710  fprodntriv  13749  divalglem7  14057  divalg  14061  gcdcllem1  14149  gcdcllem3  14151  isprm2lem  14224  pcpre1  14366  pcqmul  14377  pcqcl  14380  xpscfv  14959  xpsfrnel  14960  mreintcl  14992  isdrs  15563  isipodrs  15791  sgrp2rid2ex  16045  frgpuptinv  16789  isdrngrd  17422  isnzr2  17911  psgnodpmr  18626  lindfrn  18856  dmatelnd  18998  dmatmul  18999  mdetdiaglem  19100  mdetunilem1  19114  fvmptnn04ifa  19351  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  fiinopn  19410  hausnei  19829  dfcon2  19920  2ndcdisj  19957  regr1lem2  20241  isfbas  20330  ioorinv  21985  ioorcl  21986  vitalilem2  22018  vitalilem3  22019  vitali  22022  itg1climres  22121  mbfi1fseqlem4  22125  dvferm1lem  22385  dvferm2lem  22387  isuc1p  22541  ismon1p  22543  ply1remlem  22563  plydivlem4  22692  aannenlem1  22724  aannenlem2  22725  lgsne0  23608  lgsqr  23621  axtg5seg  23862  axtgupdim2  23869  axtgeucl  23870  axlowdim1  24262  usgranloopv  24378  usgra1v  24390  cusgrafilem2  24480  wlkn0  24527  2pthoncl  24605  iswwlk  24683  eupath2lem2  24978  eupath2lem3  24979  3cyclfrgrarn1  25012  4cycl2vnunb  25017  frgrawopreglem3  25046  norm1exi  26168  shintcl  26248  chintcl  26250  chne0  26412  elspansn2  26485  eigre  26754  eigorth  26757  kbpj  26875  superpos  27273  hatomic  27279  xrge0iifhom  27919  xrge0iif1  27920  esumpr2  28074  sibfof  28282  signswn0  28517  signswch  28518  signstfvneq0  28529  subfacp1lem1  28623  erdszelem8  28642  indispcon  28679  cvmsss2  28719  nepss  29095  frmin  29322  elwlim  29379  dfrdg4  29600  fvray  29791  linedegen  29793  fvline  29794  hilbert1.1  29804  rankeq1o  29828  itg2addnclem3  30068  neificl  30246  isdrngo3  30362  ispridl  30431  ismaxidl  30437  dnnumch1  30990  aomclem3  31002  aomclem8  31007  dfac11  31008  dfacbasgrp  31057  fnchoice  31404  idlimc  31632  limcperiod  31634  limclner  31657  fperdvper  31715  stoweidlem35  31817  stoweidlem43  31825  stoweidlem59  31841  fourierdlem76  31965  etransclem47  32064  usgvad2edg  32411  tpres  32554  nrhmzr  32679  ax6e2ndeq  33332  ax6e2ndeqVD  33709  bnj168  33785  bnj970  34005  bnj1154  34055  islshp  34704  lsatn0  34724  lshpset2N  34844  atlex  35041  hlsuprexch  35105  3dimlem1  35182  llni2  35236  lplni2  35261  2llnjN  35291  lvoli2  35305  2lplnj  35344  islinei  35464  lnatexN  35503  llnexchb2  35593  lhpmatb  35755  cdleme40m  36193  cdlemftr3  36291  cdlemk28-3  36634  cdlemk35s  36663  cdlemk39s  36665  cdlemk42  36667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
  Copyright terms: Public domain W3C validator