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

Definition df-ne 2654
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 2652 . 2
41, 2wceq 1670 . . 3
54wn 3 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  neii  2656  neir  2657  nne  2658  exmidne  2660  nonconne  2661  neeq1  2662  neeq2  2663  neneqd  2670  necon3abii  2684  necon3bii  2686  necon3abid  2687  necon3bid  2689  necon3d  2692  necon1ai  2699  necon1i  2701  necon2bd  2706  necon2d  2707  necon1abii  2708  necon1bbii  2709  necon1abid  2710  necon1bbid  2711  necon2abid  2714  necon2bbid  2715  necon4abid  2721  necon1ad  2724  neor  2741  neanior  2742  neorian  2744  nfne  2748  nfned  2749  eqneqall  2750  dfpss2  3478  neq0  3683  ifnefalse  3835  eqsn  4060  opthpr  4076  prnebg  4080  unissint  4178  iununi  4281  disji2  4305  opthneg  4594  ord0eln0  4794  unizlim  4857  frsn  4931  xpcan  5295  xpcan2  5296  xpima  5301  unixpid  5392  mpt2difsnif  6195  orduniorsuc  6451  dflim3  6468  tfindsg  6481  nn0suc  6510  findsg  6513  bropopvvv  6659  tz7.49  6864  oevn0  6921  php  7456  1sdom  7476  fimaxg  7520  fiint  7549  wemapso2lem  7686  card2on  7689  brwdomn0  7704  domwdom  7709  rankxplim2  7973  rankxplim3  7974  carden2a  8022  dfackm  8217  fin23lem14  8384  fin1a2lem12  8462  axcc2lem  8487  ac6num  8530  zorn2lem4  8550  zorn2lem7  8553  brdom3  8577  iundom2g  8586  r1tskina  8828  1re  9264  ltlen  9355  uzm1  10755  xrnemnf  10963  xrnepnf  10964  ioo0  11189  ico0  11210  ioc0  11211  icc0  11212  elfznelfzo  11479  elfznelfzob  11480  injresinjlem  11487  fleqceilz  11542  sq01  11835  hash1snb  12020  euhash1  12021  hashgt12el  12022  hashgt12el2  12023  hash2prde  12028  hash2prd  12030  hashfun  12046  swrdccatin1  12221  repswcshw  12293  cshw1  12303  sgnn  12430  incexc2  13148  sqr2irr  13378  divalglem8  13451  ndvdssub  13458  algcvgblem  13599  isprm2lem  13617  isprm3  13619  isprm4  13620  ramcl2lem  13917  cshwshashlem1  13969  cshwshash  13978  symg2bas  15684  symgextf  15698  symgextfv  15699  odlem1  15782  gexlem1  15822  dprdfeq0  16195  isnirred  16421  isirred2  16422  drngmul0or  16472  drngmuleq0  16474  lvecvs0or  16803  lvecvscan  16806  isnzr2  16959  isdomn2  16984  domnchr  17438  psgndiflemB  17698  uvcvv0  17736  mulmarep1gsum1  17852  mulmarep1gsum2  17853  mdetunilem5  17894  mdetunilem8  17897  mdetunilem9  17898  madurid  17924  elcls  18151  opnnei  18198  ist0-3  18423  ist1-2  18425  dfcon2  18497  cnconn  18500  pthaus  18685  xkohaus  18700  hausflim  19028  cldsubg  19155  bcth  20297  ioorinv  20483  tdeglem4  20998  fta1b  21107  plydivex  21229  plyexmo  21245  aalioulem3  21266  dvradcnv  21352  logtayllem  21570  logtayl  21571  cxpcl  21585  recxpcl  21586  logrec  21681  isosctrlem2  21683  efrlim  21829  muval2  21938  musum  21997  dchrelbas2  22042  dchrelbas4  22048  dchrfi  22060  dchrptlem3  22071  dchrsum2  22073  sumdchr2  22075  lgscllem  22108  2sqb  22183  dchrvmasumiflem2  22217  rpvmasum2  22227  padicabv  22345  padicabvf  22346  padicabvcxp  22347  usgra2edg  22423  usgra2edg1  22424  nbgranself  22467  nb3graprlem1  22481  uvtx01vtx  22522  wlkdvspthlem  22628  usgrcyclnl1  22648  usgrcyclnl2  22649  constr3trllem2  22659  eupath2lem1  22720  ismgm  22929  vcoprne  23079  nvmul0or  23154  nmogtmnf  23292  hvmul0or  23549  hvmulcan  23596  hvmulcan2  23597  hiidge0  23622  bcsiALT  23703  norm1exi  23775  shne0i  23973  nonbooli  24176  nmopgtmnf  24394  unopbd  24541  nmcfnlbi  24578  nmopcoi  24621  largei  24793  chirredi  24920  mdsymlem5  24933  sumdmdlem2  24945  disji2f  25049  iundisj2f  25060  imadifxp  25067  iundisj2fi  25211  ind1a  25657  ballotlemii  26036  sgn3da  26074  plymulx  26100  subfacp1lem6  26219  cvmsdisj  26305  cvmscld  26308  pm2.61iine  26525  snnzb  26741  dfrdg2  26762  wfrlem16  26892  sltval2  26950  nosgnn0  26952  nosgnn0i  26953  sltintdifex  26957  sltres  26958  sltsolem1  26962  nodenselem4  26978  nodenselem5  26979  nodenselem7  26981  nobndup  26994  nobnddown  26995  nofulllem5  27000  dfrdg4  27134  brbtwn2  27183  colinearalg  27188  axlowdimlem6  27225  axlowdimlem13  27232  axlowdimlem14  27233  axlowdim1  27237  axcontlem12  27253  btwnconn1lem13  27372  lineunray  27420  rankeq1o  27451  ordtoplem  27524  itg2addnclem3  27625  itgaddnclem2  27631  elicc3  27692  nn0prpw  27698  fdc  27821  prtlem90  28146  raldifsni  28173  cmpfiiin  28181  0dioph  28265  fphpd  28303  jm2.23  28493  wepwsolem  28542  sdrgacs  28740  isdomn3  28754  pm13.196a  28842  refsum2cnlem1  28934  fmul01lt1lem1  28940  stoweidlem14  28988  stoweidlem28  29002  stoweidlem55  29029  stoweid  29037  raaan2  29178  2reu4a  29192  afvfv0bi  29237  pr1eqbg  29302  2f1fvneq  29324  dff14a  29325  2ffzoeq  29393  wlk0  29473  wwlknext  29537  clwlkisclwwlklem2a4  29627  clwwisshclwwn  29653  clwlknclwlkdifs  29759  frgra3vlem1  29773  frgra3vlem2  29774  3vfriswmgralem  29777  2pthfrgra  29784  4cycl2vnunb  29790  n4cyclfrgra  29791  frgrancvvdeqlemA  29811  frgrancvvdeqlemB  29812  frgrancvvdeqlemC  29813  frgrawopreglem3  29820  frgrawopreglem4  29821  frgraregorufr0  29826  frgraregorufr  29827  usg2spot2nb  29839  numclwwlk3lem  29882  frgrareg  29891  frgraregord013  29892  onfrALTlem5  30096  onfrALTlem3  30098  en3lpVD  30427  onfrALTlem5VD  30467  onfrALTlem3VD  30469  a6e2ndeqVD  30491  a6e2ndeqALT  30513  isosctrlem1ALT  30516  bnj1109  30627  bnj1542  30698  bnj1253  30856  cvrval2  31622  cvrnbtwn2  31623  cvrnbtwn3  31624  cvlsupr3  31692  hlrelat5N  31748  cvrat4  31790  2at0mat0  31872  dalawlem13  32230  isltrn2N  32467  trlator0  32518  cdleme22b  32688  dochkrshp  33734  dochkrshp4  33737  lcfl6  33848  lclkrlem2x  33878
  Copyright terms: Public domain W3C validator