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

Definition df-ne 2421
Description: Define inequality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ne  |-  ( A  =/=  B  <->  -.  A  =  B )

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wne 2419 . 2  wff  A  =/= 
B
41, 2wceq 1619 . . 3  wff  A  =  B
54wn 5 . 2  wff  -.  A  =  B
63, 5wb 178 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2423  exmidne  2425  nonconne  2426  neeq1  2427  neeq2  2428  neneqd  2435  necon3abii  2449  necon3bii  2451  necon3abid  2452  necon3bid  2454  necon3d  2457  necon1ai  2461  necon1i  2463  necon2bd  2468  necon2d  2469  necon1abii  2470  necon1bbii  2471  necon1abid  2472  necon1bbid  2473  necon2abid  2476  necon2bbid  2477  necon4abid  2483  necon1ad  2486  neor  2503  neanior  2504  neorian  2506  nemtbir  2507  nfne  2512  nfned  2514  dfpss2  3222  ne0i  3422  neq0  3426  ifnefalse  3533  eqsn  3735  snsssn  3741  opthpr  3750  unissint  3846  iununi  3946  disji2  3970  ord0eln0  4404  nsuceq0  4430  unizlim  4467  orduniorsuc  4579  dflim3  4596  tfindsg  4609  nn0suc  4638  findsg  4641  frsn  4734  xpcan  5086  xpcan2  5087  unixpid  5180  fv2  5440  fvprc  5441  tz7.49  6411  oevn0  6468  2dom  6887  sdomdif  6963  2pwne  6971  map2xp  6985  mapdom2  6986  php  6999  1sdom  7019  fimaxg  7058  fiint  7087  wemapso2lem  7219  card2on  7222  brwdomn0  7237  domwdom  7242  rankxplim2  7504  rankxplim3  7505  carden2a  7553  pm54.43lem  7586  dfackm  7746  fin23lem14  7913  fin1a2lem12  7991  axcc2lem  8016  ac6num  8060  ac9  8064  ac9s  8074  zorn2lem4  8080  zorn2lem7  8083  brdom3  8107  iundom2g  8116  canthp1lem2  8229  r1tskina  8358  ax1ne0  8736  1re  8791  ltlen  8876  ine0  9169  recgt0ii  9616  inelr  9690  nnunb  9914  uzm1  10211  xrnemnf  10413  xrnepnf  10414  xrltnr  10415  pnfnlt  10420  nltmnf  10421  xrltlen  10433  ioo0  10633  ico0  10654  ioc0  10655  icc0  10656  fzm1  10814  sq01  11175  hashfun  11340  sqr2irr  12475  divalglem8  12547  ndvdssub  12554  algcvgblem  12695  isprm2lem  12713  isprm2  12714  isprm3  12715  isprm4  12716  isprm5  12739  ramcl2lem  13004  xpsfrnel2  13415  setcepi  13868  odlem1  14798  gexlem1  14838  dprdfeq0  15205  isnirred  15430  isirred2  15431  drngmul0or  15481  drngmuleq0  15483  lvecvs0or  15809  lvecvscan  15812  lspsncv0  15847  isnzr2  15963  isdomn2  15988  domnchr  16434  elcls  16758  opnnei  16805  ist0-3  17021  ist1-2  17023  dfcon2  17093  cnconn  17096  pthaus  17280  xkohaus  17295  trfbas  17487  fbunfip  17512  trfil2  17530  hausflim  17624  alexsub  17687  cldsubg  17741  bcth  18699  iundisj2  18854  ioorf  18876  ioorinv  18879  tdeglem4  19394  fta1b  19503  plydivex  19625  vieta1lem2  19639  plyexmo  19641  aalioulem3  19662  dvtaylp  19697  dvradcnv  19745  sinhalfpilem  19782  coseq1  19838  logtayllem  19954  logtayl  19955  cxpcl  19969  recxpcl  19970  logrec  20065  isosctrlem2  20067  efrlim  20212  muval2  20320  musum  20379  dchrelbas2  20424  dchrelbas4  20430  dchrfi  20442  dchrptlem3  20453  dchrsum2  20455  sumdchr2  20457  lgsfcl2  20489  lgscllem  20490  lgsval2lem  20493  2sqb  20565  dchrvmasumiflem2  20599  rpvmasum2  20609  dchrisumn0  20618  padicabv  20727  padicabvf  20728  padicabvcxp  20729  ismgm  20933  vcoprne  21081  nvmul0or  21156  nmogtmnf  21294  hvmul0or  21550  hvmulcan  21597  hvmulcan2  21598  hiidge0  21623  bcsiALT  21704  norm1exi  21775  shne0i  21973  nonbooli  22194  nmopgtmnf  22394  unopbd  22541  nmcfnlbi  22578  nmopcoi  22621  strlem1  22776  largei  22793  chirredi  22920  mdsymlem5  22933  sumdmdlem2  22945  ballotlemi1  23008  ballotlemii  23009  ballotlemfrcn0  23035  subfacp1lem6  23074  pconcon  23120  cvmsdisj  23159  cvmscld  23162  eupath2lem1  23259  eupath  23263  pm2.61iine  23438  dfrdg2  23507  wfrlem16  23626  sltval2  23664  nosgnn0  23666  nosgnn0i  23667  sltintdifex  23671  sltres  23672  axsltsolem1  23676  axdenselem3  23692  axdenselem4  23693  axdenselem5  23694  axdenselem7  23696  axfelem9  23709  axfelem10  23710  axfelem15  23715  axfelem18  23718  axfelem22  23722  dfrdg4  23849  brbtwn2  23894  colinearalg  23899  axlowdimlem6  23936  axlowdimlem13  23943  axlowdimlem14  23944  axlowdim1  23948  axcontlem12  23964  btwnconn1lem13  24083  lineunray  24131  rankeq1o  24162  ordtoplem  24235  vxveqv  24406  repcpwti  24514  dmse1  24956  iintlem1  24963  hdrmp  25059  lineval5a  25441  lineval6a  25442  lppotoslem  25496  lppotos  25497  xsyysx  25498  bsstrs  25499  nbssntrs  25500  pdiveql  25521  hpd  25522  elicc3  25581  nn0prpw  25592  fdc  25808  maxidln0  26023  prtlem90  26076  raldifsni  26106  cmpfiiin  26125  0dioph  26211  fphpd  26252  pellexlem6  26272  jm2.23  26442  wepwsolem  26491  uvcvv0  26592  sdrgacs  26862  isdomn3  26876  pm13.196a  26968  compneOLD  26997  fnchoice  27054  refsum2cnlem1  27062  fmul01lt1lem1  27068  stoweidlem14  27084  stoweidlem23  27093  stoweidlem28  27098  stoweidlem35  27105  stoweidlem39  27109  stoweidlem55  27125  stoweidlem58  27128  stoweid  27133  sgnn  27284  onfrALTlem5  27344  onfrALTlem3  27346  en3lpVD  27655  onfrALTlem5VD  27695  onfrALTlem3VD  27697  a9e2ndeqVD  27719  a9e2ndeqALT  27742  bnj1109  27851  bnj1542  27922  bnj1253  28080  cvrval2  28615  cvrnbtwn2  28616  cvrnbtwn3  28617  cvlsupr3  28685  hlrelat5N  28741  cvrat4  28783  2at0mat0  28865  dalawlem13  29223  isltrn2N  29460  trlator0  29511  cdleme22b  29681  dochkrshp  30727  dochkrshp4  30730  lcfl6  30841  lclkrlem2x  30871  hdmapip0  31259
  Copyright terms: Public domain W3C validator