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

Definition df-ne 2600
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 2598 . 2  wff  A  =/= 
B
41, 2wceq 1652 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 177 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  nne  2602  exmidne  2604  nonconne  2605  neeq1  2606  neeq2  2607  neneqd  2614  necon3abii  2628  necon3bii  2630  necon3abid  2631  necon3bid  2633  necon3d  2636  necon1ai  2640  necon1i  2642  necon2bd  2647  necon2d  2648  necon1abii  2649  necon1bbii  2650  necon1abid  2651  necon1bbid  2652  necon2abid  2655  necon2bbid  2656  necon4abid  2662  necon1ad  2665  neor  2682  neanior  2683  neorian  2685  nemtbir  2686  nfne  2689  nfned  2690  dfpss2  3424  neq0  3630  ifnefalse  3739  eqsn  3952  snsssn  3959  opthpr  3968  prnebg  3971  unissint  4066  iununi  4167  disji2  4191  ord0eln0  4627  nsuceq0  4653  unizlim  4690  orduniorsuc  4802  dflim3  4819  tfindsg  4832  nn0suc  4861  findsg  4864  frsn  4940  xpcan  5297  xpcan2  5298  xpima  5305  unixpid  5396  0neqopab  6111  bropopvvv  6418  tz7.49  6694  oevn0  6751  2dom  7171  map2xp  7269  php  7283  1sdom  7303  fimaxg  7346  fiint  7375  wemapso2lem  7511  card2on  7514  brwdomn0  7529  domwdom  7534  rankxplim2  7796  rankxplim3  7797  carden2a  7845  pm54.43lem  7878  dfackm  8038  fin23lem14  8205  fin1a2lem12  8283  axcc2lem  8308  ac6num  8351  zorn2lem4  8371  zorn2lem7  8374  brdom3  8398  iundom2g  8407  canthp1lem2  8520  r1tskina  8649  ax1ne0  9027  1re  9082  ltlen  9167  ine0  9461  recgt0ii  9908  inelr  9982  nnunb  10209  uzm1  10508  xrnemnf  10710  xrnepnf  10711  xrltnr  10712  pnfnlt  10717  nltmnf  10718  xrltlen  10731  ioo0  10933  ico0  10954  ioc0  10955  icc0  10956  fzm1  11119  elfznelfzo  11184  elfznelfzob  11185  injresinjlem  11191  sq01  11493  hash1snb  11673  hashgt12el  11674  hashgt12el2  11675  hash2prde  11680  hashfun  11692  incexc2  12610  sqr2irr  12840  divalglem8  12912  ndvdssub  12919  algcvgblem  13060  isprm2lem  13078  isprm3  13080  isprm4  13081  ramcl2lem  13369  xpsfrnel2  13782  setcepi  14235  odlem1  15165  gexlem1  15205  dprdfeq0  15572  isnirred  15797  isirred2  15798  drngmul0or  15848  drngmuleq0  15850  lvecvs0or  16172  lvecvscan  16175  lspsncv0  16210  isnzr2  16326  isdomn2  16351  domnchr  16805  elcls  17129  opnnei  17176  ist0-3  17401  ist1-2  17403  dfcon2  17474  cnconn  17477  pthaus  17662  xkohaus  17677  trfbas  17868  fbunfip  17893  trfil2  17911  hausflim  18005  cldsubg  18132  bcth  19274  iundisj2  19435  ioorinv  19460  tdeglem4  19975  fta1b  20084  plydivex  20206  vieta1lem2  20220  plyexmo  20222  aalioulem3  20243  dvradcnv  20329  sinhalfpilem  20366  coseq1  20422  logtayllem  20542  logtayl  20543  cxpcl  20557  recxpcl  20558  logrec  20653  isosctrlem2  20655  efrlim  20800  muval2  20909  musum  20968  dchrelbas2  21013  dchrelbas4  21019  dchrfi  21031  dchrptlem3  21042  dchrsum2  21044  sumdchr2  21046  lgscllem  21079  2sqb  21154  dchrvmasumiflem2  21188  rpvmasum2  21198  padicabv  21316  padicabvf  21317  padicabvcxp  21318  usgraedgprv  21388  usgra2edg  21394  usgra2edg1  21395  nbgranself  21438  nb3graprlem1  21452  uvtx01vtx  21493  2trllemA  21542  wlkntrllem3  21553  2pthon  21594  2pthon3v  21596  wlkdvspthlem  21599  usgrcyclnl1  21619  usgrcyclnl2  21620  constr3trllem2  21630  4cycl4dv  21646  eupath2lem1  21691  ismgm  21900  vcoprne  22050  nvmul0or  22125  nmogtmnf  22263  hvmul0or  22519  hvmulcan  22566  hvmulcan2  22567  hiidge0  22592  bcsiALT  22673  norm1exi  22744  shne0i  22942  nonbooli  23145  nmopgtmnf  23363  unopbd  23510  nmcfnlbi  23547  nmopcoi  23590  largei  23762  chirredi  23889  mdsymlem5  23902  sumdmdlem2  23914  disji2f  24011  iundisj2f  24022  imadifxp  24030  iundisj2fi  24145  ind1a  24410  ballotlemii  24753  subfacp1lem6  24863  cvmsdisj  24949  cvmscld  24952  pm2.61iine  25178  snnzb  25394  dfrdg2  25415  wfrlem16  25545  sltval2  25603  nosgnn0  25605  nosgnn0i  25606  sltintdifex  25610  sltres  25611  sltsolem1  25615  nodenselem4  25631  nodenselem5  25632  nodenselem7  25634  nobndup  25647  nobnddown  25648  nofulllem5  25653  dfrdg4  25787  brbtwn2  25836  colinearalg  25841  axlowdimlem6  25878  axlowdimlem13  25885  axlowdimlem14  25886  axlowdim1  25890  axcontlem12  25906  btwnconn1lem13  26025  lineunray  26073  rankeq1o  26104  ordtoplem  26177  itg2addnclem3  26248  itgaddnclem2  26254  elicc3  26311  nn0prpw  26317  fdc  26440  prtlem90  26697  raldifsni  26725  cmpfiiin  26742  0dioph  26828  fphpd  26868  jm2.23  27058  wepwsolem  27107  uvcvv0  27207  sdrgacs  27477  isdomn3  27491  pm13.196a  27582  refsum2cnlem1  27675  fmul01lt1lem1  27681  stoweidlem14  27730  stoweidlem28  27744  stoweidlem55  27771  stoweid  27779  raaan2  27920  2reu4a  27934  afvfv0bi  27983  eqneqall  28040  pr1eqbg  28046  2f1fvneq  28063  dff14a  28064  euhash1  28145  swrdccatin1  28171  2cshwmod  28223  cshw1  28238  cshwssizelem1a  28242  cshwssizelem2  28244  cshwssizelem3  28245  cshwssize  28253  frgra3vlem1  28327  frgra3vlem2  28328  3vfriswmgralem  28331  2pthfrgra  28338  4cycl2vnunb  28344  n4cyclfrgra  28345  frgrancvvdeqlemA  28363  frgrancvvdeqlemB  28364  frgrancvvdeqlemC  28365  frgrawopreglem3  28372  frgrawopreglem4  28373  frgraregorufr0  28378  frgraregorufr  28379  usg2spot2nb  28391  sgnn  28461  onfrALTlem5  28565  onfrALTlem3  28567  en3lpVD  28894  onfrALTlem5VD  28934  onfrALTlem3VD  28936  a9e2ndeqVD  28958  a9e2ndeqALT  28980  isosctrlem1ALT  28983  bnj1109  29094  bnj1542  29165  bnj1253  29323  cvrval2  30009  cvrnbtwn2  30010  cvrnbtwn3  30011  cvlsupr3  30079  hlrelat5N  30135  cvrat4  30177  2at0mat0  30259  dalawlem13  30617  isltrn2N  30854  trlator0  30905  cdleme22b  31075  dochkrshp  32121  dochkrshp4  32124  lcfl6  32235  lclkrlem2x  32265
  Copyright terms: Public domain W3C validator