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

Definition df-ne 2587
Description: Define inequality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ne

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wne 2585 . 2
41, 2wceq 1687 . . 3
54wn 3 . 2
63, 5wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  neii  2589  neir  2590  nne  2591  exmidne  2593  nonconne  2594  neeq1  2595  neeq2  2596  neneqd  2603  necon3abii  2617  necon3bii  2619  necon3abid  2620  necon3bid  2622  necon3d  2625  necon1ai  2632  necon1i  2634  necon2bd  2639  necon2d  2640  necon1abii  2641  necon1bbii  2642  necon1abid  2643  necon1bbid  2644  necon2abid  2647  necon2bbid  2648  necon4abid  2654  necon1ad  2657  pm2.61iine  2671  neor  2675  neanior  2676  neorian  2678  nfne  2682  nfned  2683  eqneqall  2684  nabbi  2685  dfpss2  3418  neq0  3624  ifnefalse  3778  snnzb  3917  raldifsni  3980  eqsn  4009  opthpr  4025  prnebg  4029  unissint  4127  iununi  4230  disji2  4254  opthneg  4543  ord0eln0  4744  unizlim  4806  frsn  4880  xpcan  5246  xpcan2  5247  xpima  5252  unixpid  5344  mpt2difsnif  6153  orduniorsuc  6411  dflim3  6428  tfindsg  6441  nn0suc  6470  findsg  6473  bropopvvv  6622  suppvalbr  6663  tz7.49  6859  oevn0  6916  php  7454  1sdom  7474  fimaxg  7518  fiint  7547  wemapsolem  7711  card2on  7716  brwdomn0  7731  domwdom  7736  rankxplim2  8034  rankxplim3  8035  carden2a  8083  dfackm  8282  fin23lem14  8449  fin1a2lem12  8527  axcc2lem  8552  ac6num  8595  zorn2lem4  8615  zorn2lem7  8618  brdom3  8642  iundom2g  8651  r1tskina  8895  1re  9331  ltlen  9422  uzm1  10836  xrnemnf  11044  xrnepnf  11045  ioo0  11270  ico0  11291  ioc0  11292  icc0  11293  elfznelfzo  11571  elfznelfzob  11572  injresinjlem  11579  fleqceilz  11634  sq01  11927  hash1snb  12112  euhash1  12113  hashgt12el  12114  hashgt12el2  12115  hash2prde  12120  hash2prd  12122  hashge2el2dif  12125  hashfun  12140  swrdccatin1  12315  repswcshw  12387  cshw1  12397  sgnn  12524  incexc2  13241  sqr2irr  13471  divalglem8  13544  ndvdssub  13551  algcvgblem  13692  isprm2lem  13710  isprm3  13712  isprm4  13713  ramcl2lem  14010  cshwshashlem1  14062  cshwshash  14071  symg2bas  15840  symgextf  15859  symgextfv  15860  odlem1  15975  gexlem1  16015  dprdfeq0  16389  isnirred  16615  isirred2  16616  drngmul0or  16666  drngmuleq0  16668  lvecvs0or  16998  lvecvscan  17001  isnzr2  17154  isdomn2  17179  domnchr  17671  psgndiflemB  17738  uvcvv0  17918  mulmarep1gsum1  18082  mulmarep1gsum2  18083  mdetunilem5  18124  mdetunilem8  18127  mdetunilem9  18128  madurid  18154  elcls  18381  opnnei  18428  ist0-3  18653  ist1-2  18655  dfcon2  18727  cnconn  18730  pthaus  18915  xkohaus  18930  hausflim  19258  cldsubg  19385  bcth  20540  ioorinv  20756  tdeglem4  21271  fta1b  21382  plydivex  21504  plyexmo  21520  aalioulem3  21541  dvradcnv  21627  logtayllem  21845  logtayl  21846  cxpcl  21860  recxpcl  21861  logrec  21956  isosctrlem2  21958  efrlim  22104  muval2  22213  musum  22272  dchrelbas2  22317  dchrelbas4  22323  dchrfi  22335  dchrptlem3  22346  dchrsum2  22348  sumdchr2  22350  lgscllem  22383  2sqb  22458  dchrvmasumiflem2  22492  rpvmasum2  22502  padicabv  22620  padicabvf  22621  padicabvcxp  22622  tglowdim1i  22692  tgbtwnconn1  22739  colline  22774  brbtwn2  22830  colinearalg  22835  axlowdimlem6  22872  axlowdimlem13  22879  axlowdimlem14  22880  axlowdim1  22884  axcontlem12  22900  usgra2edg  22980  usgra2edg1  22981  nbgranself  23024  nb3graprlem1  23038  uvtx01vtx  23079  wlkdvspthlem  23185  usgrcyclnl1  23205  usgrcyclnl2  23206  constr3trllem2  23216  eupath2lem1  23277  ismgm  23486  vcoprne  23636  nvmul0or  23711  nmogtmnf  23849  hvmul0or  24106  hvmulcan  24153  hvmulcan2  24154  hiidge0  24179  bcsiALT  24260  norm1exi  24332  shne0i  24530  nonbooli  24733  nmopgtmnf  24951  unopbd  25098  nmcfnlbi  25135  nmopcoi  25178  largei  25350  chirredi  25477  mdsymlem5  25490  sumdmdlem2  25502  disji2f  25601  iundisj2f  25612  imadifxp  25619  iundisj2fi  25759  ind1a  26186  ballotlemii  26589  sgn3da  26627  plymulx  26652  subfacp1lem6  26776  cvmsdisj  26862  cvmscld  26865  dfrdg2  27311  wfrlem16  27441  sltval2  27499  nosgnn0  27501  nosgnn0i  27502  sltintdifex  27506  sltres  27507  sltsolem1  27511  nodenselem4  27527  nodenselem5  27528  nodenselem7  27530  nobndup  27543  nobnddown  27544  nofulllem5  27549  dfrdg4  27683  btwnconn1lem13  27832  lineunray  27880  rankeq1o  27911  ordtoplem  27984  itg2addnclem3  28116  itgaddnclem2  28122  elicc3  28183  nn0prpw  28189  fdc  28312  prtlem90  28674  cmpfiiin  28705  0dioph  28790  fphpd  28828  jm2.23  29018  wepwsolem  29067  sdrgacs  29231  isdomn3  29245  pm13.196a  29341  refsum2cnlem1  29432  fmul01lt1lem1  29438  stoweidlem14  29483  stoweidlem28  29497  stoweidlem55  29524  stoweid  29532  raaan2  29673  2reu4a  29687  afvfv0bi  29732  pr1eqbg  29795  2f1fvneq  29817  dff14a  29818  2ffzoeq  29888  wlk0  29966  wwlknext  30030  clwlkisclwwlklem2a4  30120  clwwisshclwwn  30146  clwlknclwlkdifs  30252  frgra3vlem1  30266  frgra3vlem2  30267  3vfriswmgralem  30270  2pthfrgra  30277  4cycl2vnunb  30283  n4cyclfrgra  30284  frgrancvvdeqlemA  30304  frgrancvvdeqlemB  30305  frgrancvvdeqlemC  30306  frgrawopreglem3  30313  frgrawopreglem4  30314  frgraregorufr0  30319  frgraregorufr  30320  usg2spot2nb  30332  numclwwlk3lem  30375  frgrareg  30384  frgraregord013  30385  fdmdifeqresdif  30404  pgrpgt2nabel  30431  islindeps  30571  lincext1  30572  lindslinindsimp2lem5  30580  snlindsntor  30589  ldepslinc  30635  onfrALTlem5  30827  onfrALTlem3  30829  en3lpVD  31159  onfrALTlem5VD  31199  onfrALTlem3VD  31201  ax6e2ndeqVD  31223  ax6e2ndeqALT  31245  isosctrlem1ALT  31248  bnj1109  31358  bnj1542  31428  bnj1253  31586  cvrval2  32356  cvrnbtwn2  32357  cvrnbtwn3  32358  cvlsupr3  32426  hlrelat5N  32482  cvrat4  32524  2at0mat0  32606  dalawlem13  32964  isltrn2N  33201  trlator0  33252  cdleme22b  33422  dochkrshp  34468  dochkrshp4  34471  lcfl6  34582  lclkrlem2x  34612
  Copyright terms: Public domain W3C validator