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  24222  wfrlem16  24341  sltval2  24380  nosgnn0  24382  nosgnn0i  24383  sltintdifex  24387  sltres  24388  sltsolem1  24392  nodenselem3  24407  nodenselem4  24408  nodenselem5  24409  nodenselem7  24411  nobndup  24424  nobnddown  24425  nofulllem5  24430  dfrdg4  24559  brbtwn2  24604  colinearalg  24609  axlowdimlem6  24646  axlowdimlem13  24653  axlowdimlem14  24654  axlowdim1  24658  axcontlem12  24674  btwnconn1lem13  24793  lineunray  24841  rankeq1o  24872  ordtoplem  24945  itg2addnc  25004  vxveqv  25156  repcpwti  25263  dmse1  25705  iintlem1  25712  hdrmp  25808  lineval5a  26190  lineval6a  26191  lppotoslem  26245  lppotos  26246  xsyysx  26247  bsstrs  26248  nbssntrs  26249  pdiveql  26270  hpd  26271  elicc3  26330  nn0prpw  26341  fdc  26557  maxidln0  26772  prtlem90  26825  raldifsni  26855  cmpfiiin  26874  0dioph  26960  fphpd  27001  pellexlem6  27021  jm2.23  27191  wepwsolem  27240  uvcvv0  27341  sdrgacs  27611  isdomn3  27625  pm13.196a  27716  compneOLD  27745  fnchoice  27802  refsum2cnlem1  27810  fmul01lt1lem1  27816  stoweidlem14  27865  stoweidlem23  27874  stoweidlem28  27879  stoweidlem35  27886  stoweidlem39  27890  stoweidlem55  27906  stoweidlem58  27909  stoweid  27914  raaan2  28055  2reu4a  28069  afvfv0bi  28119  0neqopab  28191  elfznelfzo  28212  injresinjlem  28213  hashgt12el  28217  hashgt12el2  28218  usgraedgprv  28255  nbusgra  28276  nbgranself  28282  nb3graprlem1  28286  uvtx01vtx  28304  trlonprop  28340  wlkntrllem2  28345  wlkntrllem5  28348  wlkdvspthlem  28364  usgrcyclnl1  28385  usgrcyclnl2  28386  constr3trllem2  28396  4cycl4dv  28412  frgra3vlem1  28423  frgra3vlem2  28424  3vfriswmgralem  28427  4cycl2vnunb  28438  n4cyclfrgra  28439  sgnn  28504  onfrALTlem5  28605  onfrALTlem3  28607  en3lpVD  28936  onfrALTlem5VD  28976  onfrALTlem3VD  28978  a9e2ndeqVD  29000  a9e2ndeqALT  29023  bnj1109  29133  bnj1542  29204  bnj1253  29362  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