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

Definition df-ne 2545
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 2543 . 2  wff  A  =/= 
B
41, 2wceq 1649 . . 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  2547  exmidne  2549  nonconne  2550  neeq1  2551  neeq2  2552  neneqd  2559  necon3abii  2573  necon3bii  2575  necon3abid  2576  necon3bid  2578  necon3d  2581  necon1ai  2585  necon1i  2587  necon2bd  2592  necon2d  2593  necon1abii  2594  necon1bbii  2595  necon1abid  2596  necon1bbid  2597  necon2abid  2600  necon2bbid  2601  necon4abid  2607  necon1ad  2610  neor  2627  neanior  2628  neorian  2630  nemtbir  2631  nfne  2634  nfned  2635  dfpss2  3368  neq0  3574  ifnefalse  3683  eqsn  3896  snsssn  3902  opthpr  3911  prnebg  3914  unissint  4009  iununi  4109  disji2  4133  ord0eln0  4569  nsuceq0  4595  unizlim  4631  orduniorsuc  4743  dflim3  4760  tfindsg  4773  nn0suc  4802  findsg  4805  frsn  4881  xpcan  5238  xpcan2  5239  xpima  5246  unixpid  5337  0neqopab  6051  bropopvvv  6358  tz7.49  6631  oevn0  6688  2dom  7108  map2xp  7206  php  7220  1sdom  7240  fimaxg  7283  fiint  7312  wemapso2lem  7445  card2on  7448  brwdomn0  7463  domwdom  7468  rankxplim2  7730  rankxplim3  7731  carden2a  7779  pm54.43lem  7812  dfackm  7972  fin23lem14  8139  fin1a2lem12  8217  axcc2lem  8242  ac6num  8285  zorn2lem4  8305  zorn2lem7  8308  brdom3  8332  iundom2g  8341  canthp1lem2  8454  r1tskina  8583  ax1ne0  8961  1re  9016  ltlen  9101  ine0  9394  recgt0ii  9841  inelr  9915  nnunb  10142  uzm1  10441  xrnemnf  10643  xrnepnf  10644  xrltnr  10645  pnfnlt  10650  nltmnf  10651  xrltlen  10664  ioo0  10866  ico0  10887  ioc0  10888  icc0  10889  fzm1  11050  elfznelfzo  11112  elfznelfzob  11113  injresinjlem  11119  sq01  11421  hash1snb  11601  hashgt12el  11602  hashgt12el2  11603  hash2prde  11608  hashfun  11620  incexc2  12538  sqr2irr  12768  divalglem8  12840  ndvdssub  12847  algcvgblem  12988  isprm2lem  13006  isprm3  13008  isprm4  13009  ramcl2lem  13297  xpsfrnel2  13710  setcepi  14163  odlem1  15093  gexlem1  15133  dprdfeq0  15500  isnirred  15725  isirred2  15726  drngmul0or  15776  drngmuleq0  15778  lvecvs0or  16100  lvecvscan  16103  lspsncv0  16138  isnzr2  16254  isdomn2  16279  domnchr  16729  elcls  17053  opnnei  17100  ist0-3  17324  ist1-2  17326  dfcon2  17396  cnconn  17399  pthaus  17584  xkohaus  17599  trfbas  17790  fbunfip  17815  trfil2  17833  hausflim  17927  cldsubg  18054  bcth  19144  iundisj2  19303  ioorinv  19328  tdeglem4  19843  fta1b  19952  plydivex  20074  vieta1lem2  20088  plyexmo  20090  aalioulem3  20111  dvradcnv  20197  sinhalfpilem  20234  coseq1  20290  logtayllem  20410  logtayl  20411  cxpcl  20425  recxpcl  20426  logrec  20521  isosctrlem2  20523  efrlim  20668  muval2  20777  musum  20836  dchrelbas2  20881  dchrelbas4  20887  dchrfi  20899  dchrptlem3  20910  dchrsum2  20912  sumdchr2  20914  lgscllem  20947  2sqb  21022  dchrvmasumiflem2  21056  rpvmasum2  21066  padicabv  21184  padicabvf  21185  padicabvcxp  21186  usgraedgprv  21256  usgra2edg  21261  usgra2edg1  21262  nbusgra  21299  nbgranself  21305  nb3graprlem1  21319  uvtx01vtx  21360  wlkntrllem2  21407  wlkntrllem5  21410  2trllem1  21435  2pthon  21443  2pthon3v  21445  wlkdvspthlem  21448  usgrcyclnl1  21468  usgrcyclnl2  21469  constr3trllem2  21479  4cycl4dv  21495  eupath2lem1  21540  ismgm  21749  vcoprne  21899  nvmul0or  21974  nmogtmnf  22112  hvmul0or  22368  hvmulcan  22415  hvmulcan2  22416  hiidge0  22441  bcsiALT  22522  norm1exi  22593  shne0i  22791  nonbooli  22994  nmopgtmnf  23212  unopbd  23359  nmcfnlbi  23396  nmopcoi  23439  largei  23611  chirredi  23738  mdsymlem5  23751  sumdmdlem2  23763  disji2f  23856  iundisj2f  23866  imadifxp  23874  iundisj2fi  23984  ind1a  24207  ballotlemii  24533  subfacp1lem6  24643  cvmsdisj  24729  cvmscld  24732  pm2.61iine  24958  dfrdg2  25169  wfrlem16  25288  sltval2  25327  nosgnn0  25329  nosgnn0i  25330  sltintdifex  25334  sltres  25335  sltsolem1  25339  nodenselem4  25355  nodenselem5  25356  nodenselem7  25358  nobndup  25371  nobnddown  25372  nofulllem5  25377  dfrdg4  25506  brbtwn2  25551  colinearalg  25556  axlowdimlem6  25593  axlowdimlem13  25600  axlowdimlem14  25601  axlowdim1  25605  axcontlem12  25621  btwnconn1lem13  25740  lineunray  25788  rankeq1o  25819  ordtoplem  25892  itg2addnc  25952  elicc3  26004  nn0prpw  26010  fdc  26133  prtlem90  26390  raldifsni  26418  cmpfiiin  26435  0dioph  26521  fphpd  26561  jm2.23  26751  wepwsolem  26800  uvcvv0  26901  sdrgacs  27171  isdomn3  27185  pm13.196a  27276  refsum2cnlem1  27369  fmul01lt1lem1  27375  stoweidlem14  27424  stoweidlem28  27438  stoweidlem55  27465  stoweid  27473  raaan2  27614  2reu4a  27628  afvfv0bi  27678  frgra3vlem1  27746  frgra3vlem2  27747  3vfriswmgralem  27750  2pthfrgra  27757  4cycl2vnunb  27763  n4cyclfrgra  27764  frgrancvvdeqlemA  27782  frgrancvvdeqlemB  27783  frgrancvvdeqlemC  27784  frgrawopreglem3  27791  frgrawopreglem4  27792  frgraregorufr0  27797  frgraregorufr  27798  sgnn  27863  onfrALTlem5  27964  onfrALTlem3  27966  en3lpVD  28291  onfrALTlem5VD  28331  onfrALTlem3VD  28333  a9e2ndeqVD  28355  a9e2ndeqALT  28378  bnj1109  28488  bnj1542  28559  bnj1253  28717  cvrval2  29440  cvrnbtwn2  29441  cvrnbtwn3  29442  cvlsupr3  29510  hlrelat5N  29566  cvrat4  29608  2at0mat0  29690  dalawlem13  30048  isltrn2N  30285  trlator0  30336  cdleme22b  30506  dochkrshp  31552  dochkrshp4  31555  lcfl6  31666  lclkrlem2x  31696
  Copyright terms: Public domain W3C validator