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, 26-May-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 1395 . . 3
54wn 3 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  neii  2656  neir  2657  nne  2658  neneqd  2659  neqned  2660  exmidne  2662  exmidneOLD  2663  eqneqall  2664  nonconneOLD  2666  necon2bd  2672  necon1adOLD  2674  necon1bd  2675  necon3d  2681  necon2d  2683  necon1aiOLD  2689  necon1bi  2690  necon1i  2699  necon3abid  2703  necon1abidOLD  2706  necon1bbid  2707  necon4abidOLD  2709  necon2abidOLD  2712  necon2bbidOLD  2714  necon3bid  2715  necon3abii  2717  necon1abiiOLD  2720  necon1bbiiOLD  2722  necon3bii  2725  neeq1OLD  2739  neeq2OLD  2741  pm2.61iineOLD  2780  neor  2781  neanior  2782  neorian  2784  nfne  2788  nfned  2789  nabbi  2790  nabbiOLD  2791  dfpss2  3588  neq0  3795  ifnefalse  3953  snnzb  4094  raldifsni  4160  eqsn  4191  opthpr  4208  unissint  4311  iununi  4415  disji2  4439  opthneg  4731  ord0eln0  4937  unizlim  4999  frsn  5075  xpcan  5448  xpcan2  5449  xpima  5454  unixpid  5547  dff14a  6177  mpt2difsnif  6395  orduniorsuc  6665  dflim3  6682  tfindsg  6695  nn0suc  6724  findsg  6727  suppvalbr  6922  tz7.49  7129  oevn0  7184  php  7721  1sdom  7742  fimaxg  7787  fiint  7817  wemapsolem  7996  card2on  8001  brwdomn0  8016  domwdom  8021  rankxplim2  8319  rankxplim3  8320  carden2a  8368  dfackm  8567  fin23lem14  8734  fin1a2lem12  8812  axcc2lem  8837  ac6num  8880  zorn2lem4  8900  zorn2lem7  8903  brdom3  8927  iundom2g  8936  r1tskina  9181  1re  9616  ltlen  9707  uzm1  11140  xrnemnf  11357  xrnepnf  11358  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  elfznelfzo  11915  elfznelfzob  11916  injresinjlem  11925  fleqceilz  11981  fsuppmapnn0fiubex  12098  sq01  12288  hash1snb  12479  hashgt12el  12481  hashgt12el2  12482  hashfun  12495  hash2prde  12516  hash2prd  12518  hashge2el2dif  12521  swrdccatin1  12708  repswcshw  12780  cshw1  12790  incexc2  13650  sqrt2irr  13982  divalglem8  14058  ndvdssub  14065  algcvgblem  14206  isprm2lem  14224  isprm3  14226  isprm4  14227  ramcl2lem  14527  cshwshashlem1  14580  cshwshash  14589  isnsgrp  15915  isnmnd  15924  sgrp2nmndlem3  16043  sgrp2rid2  16044  sgrp2nmndlem5  16047  symg2bas  16423  symgextf  16442  symgextfv  16443  odlem1  16559  gexlem1  16599  dprdfeq0  17062  dprdfeq0OLD  17069  isnirred  17349  isirred2  17350  drngmul0or  17417  drngmuleq0  17419  lvecvs0or  17754  lvecvscan  17757  isnzr2  17911  isdomn2  17948  cply1mul  18335  gsummoncoe1  18346  domnchr  18569  psgndiflemB  18636  dmatmul  18999  mulmarep1gsum1  19075  mulmarep1gsum2  19076  mdetdiag  19101  mdetunilem8  19121  mdetunilem9  19122  madurid  19146  mp2pm2mplem4  19310  fvmptnn04if  19350  fvmptnn04ifb  19352  elcls  19574  opnnei  19621  ist0-3  19846  ist1-2  19848  dfcon2  19920  cnconn  19923  pthaus  20139  xkohaus  20154  hausflim  20482  cldsubg  20609  bcth  21768  ioorinv  21985  tdeglem4  22458  fta1b  22570  plydivex  22693  plyexmo  22709  aalioulem3  22730  dvradcnv  22816  logtayllem  23040  logtayl  23041  cxpcl  23055  recxpcl  23056  logrec  23151  isosctrlem2  23153  efrlim  23299  muval2  23408  musum  23467  dchrelbas2  23512  dchrelbas4  23518  dchrfi  23530  dchrptlem3  23541  dchrsum2  23543  sumdchr2  23545  lgscllem  23578  2sqb  23653  dchrvmasumiflem2  23687  rpvmasum2  23697  padicabv  23815  padicabvf  23816  padicabvcxp  23817  tglowdim1i  23892  tgbtwnconn1  23962  colline  24030  colmid  24065  lmimid  24159  lmiisolem  24161  brbtwn2  24208  colinearalg  24213  axlowdimlem6  24250  axlowdimlem14  24258  axcontlem12  24278  usgra2edg1  24383  nbgranself  24434  nb3graprlem1  24451  uvtx01vtx  24492  wlkdvspthlem  24609  usgrcyclnl1  24640  usgrcyclnl2  24641  constr3trllem2  24651  wwlknext  24724  clwlkisclwwlklem2a4  24784  clwwisshclwwn  24808  clwlknclwlkdifs  24960  eupath2lem1  24977  frgra3vlem1  25000  frgra3vlem2  25001  3vfriswmgralem  25004  2pthfrgra  25011  4cycl2vnunb  25017  n4cyclfrgra  25018  frgrancvvdeqlemA  25037  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgraregorufr0  25052  frgraregorufr  25053  numclwwlk3lem  25108  frgrareg  25117  frgraregord013  25118  ismgmOLD  25322  nvmul0or  25547  nmogtmnf  25685  hvmul0or  25942  hvmulcan  25989  hvmulcan2  25990  hiidge0  26015  bcsiALT  26096  shne0i  26366  nonbooli  26569  nmopgtmnf  26787  unopbd  26934  nmcfnlbi  26971  nmopcoi  27014  chirredi  27313  mdsymlem5  27326  sumdmdlem2  27338  disji2f  27438  imadifxp  27458  2sqcoprm  27635  sgn3da  28480  plymulx  28505  subfacp1lem6  28629  cvmsdisj  28715  wfrlem16  29358  sltval2  29416  sltres  29424  nodenselem4  29444  nodenselem5  29445  nodenselem7  29447  nobndup  29460  nobnddown  29461  nofulllem5  29466  btwnconn1lem13  29749  lineunray  29797  rankeq1o  29828  ordtoplem  29900  itg2addnclem3  30068  itgaddnclem2  30074  elicc3  30135  nn0prpw  30141  fdc  30238  prtlem90  30598  fphpd  30750  jm2.23  30938  sdrgacs  31150  isdomn3  31164  lcmcllem  31202  pm13.196a  31321  cncfiooicclem1  31696  iblcncfioo  31777  stoweidlem28  31810  raaan2  32180  2reu4a  32194  afvfv0bi  32237  pr1eqbg  32297  2f1fvneq  32307  2ffzoeq  32341  usg2edgneu  32412  copisnmnd  32497  fdmdifeqresdif  32931  pgrpgt2nabl  32959  islindeps  33054  lincext1  33055  lindslinindsimp2lem5  33063  snlindsntor  33072  ldepslinc  33110  onfrALTlem5  33314  onfrALTlem3  33316  en3lpVD  33645  onfrALTlem5VD  33685  onfrALTlem3VD  33687  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  isosctrlem1ALT  33734  bnj1109  33845  bnj1542  33915  bnj1253  34073  cvrval2  34999  cvrnbtwn2  35000  cvrnbtwn3  35001  cvlsupr3  35069  cvrat4  35167  2at0mat0  35249  dalawlem13  35607  isltrn2N  35844  trlator0  35896  cdleme22b  36067  dochkrshp  37113  dochkrshp4  37116  lcfl6  37227  lclkrlem2x  37257  xptrrel  37775
  Copyright terms: Public domain W3C validator