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

Definition df-ne 2461
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 2459 . 2  wff  A  =/= 
B
41, 2wceq 1632 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 176 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2463  exmidne  2465  nonconne  2466  neeq1  2467  neeq2  2468  neneqd  2475  necon3abii  2489  necon3bii  2491  necon3abid  2492  necon3bid  2494  necon3d  2497  necon1ai  2501  necon1i  2503  necon2bd  2508  necon2d  2509  necon1abii  2510  necon1bbii  2511  necon1abid  2512  necon1bbid  2513  necon2abid  2516  necon2bbid  2517  necon4abid  2523  necon1ad  2526  neor  2543  neanior  2544  neorian  2546  nemtbir  2547  nfne  2552  nfned  2554  dfpss2  3274  ne0i  3474  neq0  3478  ifnefalse  3586  eqsn  3791  snsssn  3797  opthpr  3806  unissint  3902  iununi  4002  disji2  4026  ord0eln0  4462  nsuceq0  4488  unizlim  4525  orduniorsuc  4637  dflim3  4654  tfindsg  4667  nn0suc  4696  findsg  4699  frsn  4776  xpcan  5128  xpcan2  5129  unixpid  5223  tz7.49  6473  oevn0  6530  2dom  6949  sdomdif  7025  2pwne  7033  map2xp  7047  mapdom2  7048  php  7061  1sdom  7081  fimaxg  7120  fiint  7149  wemapso2lem  7281  card2on  7284  brwdomn0  7299  domwdom  7304  rankxplim2  7566  rankxplim3  7567  carden2a  7615  pm54.43lem  7648  dfackm  7808  fin23lem14  7975  fin1a2lem12  8053  axcc2lem  8078  ac6num  8122  ac9  8126  ac9s  8136  zorn2lem4  8142  zorn2lem7  8145  brdom3  8169  iundom2g  8178  canthp1lem2  8291  r1tskina  8420  ax1ne0  8798  1re  8853  ltlen  8938  ine0  9231  recgt0ii  9678  inelr  9752  nnunb  9977  uzm1  10274  xrnemnf  10476  xrnepnf  10477  xrltnr  10478  pnfnlt  10483  nltmnf  10484  xrltlen  10496  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  fzm1  10878  sq01  11239  hashfun  11405  incexc2  12313  sqr2irr  12543  divalglem8  12615  ndvdssub  12622  algcvgblem  12763  isprm2lem  12781  isprm2  12782  isprm3  12783  isprm4  12784  isprm5  12807  ramcl2lem  13072  xpsfrnel2  13483  setcepi  13936  odlem1  14866  gexlem1  14906  dprdfeq0  15273  isnirred  15498  isirred2  15499  drngmul0or  15549  drngmuleq0  15551  lvecvs0or  15877  lvecvscan  15880  lspsncv0  15915  isnzr2  16031  isdomn2  16056  domnchr  16502  elcls  16826  opnnei  16873  ist0-3  17089  ist1-2  17091  dfcon2  17161  cnconn  17164  pthaus  17348  xkohaus  17363  trfbas  17555  fbunfip  17580  trfil2  17598  hausflim  17692  alexsub  17755  cldsubg  17809  bcth  18767  iundisj2  18922  ioorf  18944  ioorinv  18947  tdeglem4  19462  fta1b  19571  plydivex  19693  vieta1lem2  19707  plyexmo  19709  aalioulem3  19730  dvtaylp  19765  dvradcnv  19813  sinhalfpilem  19850  coseq1  19906  logtayllem  20022  logtayl  20023  cxpcl  20037  recxpcl  20038  logrec  20133  isosctrlem2  20135  efrlim  20280  muval2  20388  musum  20447  dchrelbas2  20492  dchrelbas4  20498  dchrfi  20510  dchrptlem3  20521  dchrsum2  20523  sumdchr2  20525  lgsfcl2  20557  lgscllem  20558  lgsval2lem  20561  2sqb  20633  dchrvmasumiflem2  20667  rpvmasum2  20677  dchrisumn0  20686  padicabv  20795  padicabvf  20796  padicabvcxp  20797  ismgm  21003  vcoprne  21151  nvmul0or  21226  nmogtmnf  21364  hvmul0or  21620  hvmulcan  21667  hvmulcan2  21668  hiidge0  21693  bcsiALT  21774  norm1exi  21845  shne0i  22043  nonbooli  22246  nmopgtmnf  22464  unopbd  22611  nmcfnlbi  22648  nmopcoi  22691  strlem1  22846  largei  22863  chirredi  22990  mdsymlem5  23003  sumdmdlem2  23015  ballotlemi1  23077  ballotlemii  23078  ballotlemfrcn0  23104  xpima  23217  disji2f  23369  disjif2  23373  iundisj2fi  23379  iundisj2f  23381  itgmcntTMP  23603  ind1a  23619  subfacp1lem6  23731  pconcon  23777  cvmsdisj  23816  cvmscld  23819  eupath2lem1  23916  eupath  23920  pm2.61iine  24096  dfrdg2  24223  wfrlem16  24342  sltval2  24381  nosgnn0  24383  nosgnn0i  24384  sltintdifex  24388  sltres  24389  sltsolem1  24393  nodenselem3  24408  nodenselem4  24409  nodenselem5  24410  nodenselem7  24412  nobndup  24425  nobnddown  24426  nofulllem5  24431  dfrdg4  24560  brbtwn2  24605  colinearalg  24610  axlowdimlem6  24647  axlowdimlem13  24654  axlowdimlem14  24655  axlowdim1  24659  axcontlem12  24675  btwnconn1lem13  24794  lineunray  24842  rankeq1o  24873  ordtoplem  24946  itg2addnc  25005  vxveqv  25157  repcpwti  25264  dmse1  25706  iintlem1  25713  hdrmp  25809  lineval5a  26191  lineval6a  26192  lppotoslem  26246  lppotos  26247  xsyysx  26248  bsstrs  26249  nbssntrs  26250  pdiveql  26271  hpd  26272  elicc3  26331  nn0prpw  26342  fdc  26558  maxidln0  26773  prtlem90  26826  raldifsni  26856  cmpfiiin  26875  0dioph  26961  fphpd  27002  pellexlem6  27022  jm2.23  27192  wepwsolem  27241  uvcvv0  27342  sdrgacs  27612  isdomn3  27626  pm13.196a  27717  compneOLD  27746  fnchoice  27803  refsum2cnlem1  27811  fmul01lt1lem1  27817  stoweidlem14  27866  stoweidlem23  27875  stoweidlem28  27880  stoweidlem35  27887  stoweidlem39  27891  stoweidlem55  27907  stoweidlem58  27910  stoweid  27915  raaan2  28056  2reu4a  28070  afvfv0bi  28120  0neqopab  28192  elfznelfzo  28213  injresinjlem  28214  hashgt12el  28218  hashgt12el2  28219  usgraedgprv  28256  nbusgra  28277  nbgranself  28283  nb3graprlem1  28287  uvtx01vtx  28305  trlonprop  28341  wlkntrllem2  28346  wlkntrllem5  28349  wlkdvspthlem  28365  usgrcyclnl1  28386  usgrcyclnl2  28387  constr3trllem2  28397  4cycl4dv  28413  frgra3vlem1  28424  frgra3vlem2  28425  3vfriswmgralem  28428  4cycl2vnunb  28439  n4cyclfrgra  28440  sgnn  28505  onfrALTlem5  28606  onfrALTlem3  28608  en3lpVD  28937  onfrALTlem5VD  28977  onfrALTlem3VD  28979  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj1109  29134  bnj1542  29205  bnj1253  29363  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn3  30088  cvlsupr3  30156  hlrelat5N  30212  cvrat4  30254  2at0mat0  30336  dalawlem13  30694  isltrn2N  30931  trlator0  30982  cdleme22b  31152  dochkrshp  32198  dochkrshp4  32201  lcfl6  32312  lclkrlem2x  32342  hdmapip0  32730
  Copyright terms: Public domain W3C validator