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

Definition df-ne 2552
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 2550 . 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  2554  exmidne  2556  nonconne  2557  neeq1  2558  neeq2  2559  neneqd  2566  necon3abii  2580  necon3bii  2582  necon3abid  2583  necon3bid  2585  necon3d  2588  necon1ai  2592  necon1i  2594  necon2bd  2599  necon2d  2600  necon1abii  2601  necon1bbii  2602  necon1abid  2603  necon1bbid  2604  necon2abid  2607  necon2bbid  2608  necon4abid  2614  necon1ad  2617  neor  2634  neanior  2635  neorian  2637  nemtbir  2638  nfne  2641  nfned  2642  dfpss2  3375  neq0  3581  ifnefalse  3690  eqsn  3903  snsssn  3909  opthpr  3918  prnebg  3921  unissint  4016  iununi  4116  disji2  4140  ord0eln0  4576  nsuceq0  4602  unizlim  4638  orduniorsuc  4750  dflim3  4767  tfindsg  4780  nn0suc  4809  findsg  4812  frsn  4888  xpcan  5245  xpcan2  5246  xpima  5253  unixpid  5344  0neqopab  6058  bropopvvv  6365  tz7.49  6638  oevn0  6695  2dom  7115  map2xp  7213  php  7227  1sdom  7247  fimaxg  7290  fiint  7319  wemapso2lem  7452  card2on  7455  brwdomn0  7470  domwdom  7475  rankxplim2  7737  rankxplim3  7738  carden2a  7786  pm54.43lem  7819  dfackm  7979  fin23lem14  8146  fin1a2lem12  8224  axcc2lem  8249  ac6num  8292  zorn2lem4  8312  zorn2lem7  8315  brdom3  8339  iundom2g  8348  canthp1lem2  8461  r1tskina  8590  ax1ne0  8968  1re  9023  ltlen  9108  ine0  9401  recgt0ii  9848  inelr  9922  nnunb  10149  uzm1  10448  xrnemnf  10650  xrnepnf  10651  xrltnr  10652  pnfnlt  10657  nltmnf  10658  xrltlen  10671  ioo0  10873  ico0  10894  ioc0  10895  icc0  10896  fzm1  11057  elfznelfzo  11119  elfznelfzob  11120  injresinjlem  11126  sq01  11428  hash1snb  11608  hashgt12el  11609  hashgt12el2  11610  hash2prde  11615  hashfun  11627  incexc2  12545  sqr2irr  12775  divalglem8  12847  ndvdssub  12854  algcvgblem  12995  isprm2lem  13013  isprm3  13015  isprm4  13016  ramcl2lem  13304  xpsfrnel2  13717  setcepi  14170  odlem1  15100  gexlem1  15140  dprdfeq0  15507  isnirred  15732  isirred2  15733  drngmul0or  15783  drngmuleq0  15785  lvecvs0or  16107  lvecvscan  16110  lspsncv0  16145  isnzr2  16261  isdomn2  16286  domnchr  16736  elcls  17060  opnnei  17107  ist0-3  17331  ist1-2  17333  dfcon2  17403  cnconn  17406  pthaus  17591  xkohaus  17606  trfbas  17797  fbunfip  17822  trfil2  17840  hausflim  17934  cldsubg  18061  bcth  19151  iundisj2  19310  ioorinv  19335  tdeglem4  19850  fta1b  19959  plydivex  20081  vieta1lem2  20095  plyexmo  20097  aalioulem3  20118  dvradcnv  20204  sinhalfpilem  20241  coseq1  20297  logtayllem  20417  logtayl  20418  cxpcl  20432  recxpcl  20433  logrec  20528  isosctrlem2  20530  efrlim  20675  muval2  20784  musum  20843  dchrelbas2  20888  dchrelbas4  20894  dchrfi  20906  dchrptlem3  20917  dchrsum2  20919  sumdchr2  20921  lgscllem  20954  2sqb  21029  dchrvmasumiflem2  21063  rpvmasum2  21073  padicabv  21191  padicabvf  21192  padicabvcxp  21193  usgraedgprv  21263  usgra2edg  21268  usgra2edg1  21269  nbusgra  21306  nbgranself  21312  nb3graprlem1  21326  uvtx01vtx  21367  wlkntrllem2  21414  wlkntrllem5  21417  2trllem1  21442  2pthon  21450  2pthon3v  21452  wlkdvspthlem  21455  usgrcyclnl1  21475  usgrcyclnl2  21476  constr3trllem2  21486  4cycl4dv  21502  eupath2lem1  21547  ismgm  21756  vcoprne  21906  nvmul0or  21981  nmogtmnf  22119  hvmul0or  22375  hvmulcan  22422  hvmulcan2  22423  hiidge0  22448  bcsiALT  22529  norm1exi  22600  shne0i  22798  nonbooli  23001  nmopgtmnf  23219  unopbd  23366  nmcfnlbi  23403  nmopcoi  23446  largei  23618  chirredi  23745  mdsymlem5  23758  sumdmdlem2  23770  disji2f  23863  iundisj2f  23873  imadifxp  23881  iundisj2fi  23991  ind1a  24214  ballotlemii  24540  subfacp1lem6  24650  cvmsdisj  24736  cvmscld  24739  pm2.61iine  24965  dfrdg2  25176  wfrlem16  25295  sltval2  25334  nosgnn0  25336  nosgnn0i  25337  sltintdifex  25341  sltres  25342  sltsolem1  25346  nodenselem4  25362  nodenselem5  25363  nodenselem7  25365  nobndup  25378  nobnddown  25379  nofulllem5  25384  dfrdg4  25513  brbtwn2  25558  colinearalg  25563  axlowdimlem6  25600  axlowdimlem13  25607  axlowdimlem14  25608  axlowdim1  25612  axcontlem12  25628  btwnconn1lem13  25747  lineunray  25795  rankeq1o  25826  ordtoplem  25899  itg2addnc  25959  elicc3  26011  nn0prpw  26017  fdc  26140  prtlem90  26397  raldifsni  26425  cmpfiiin  26442  0dioph  26528  fphpd  26568  jm2.23  26758  wepwsolem  26807  uvcvv0  26908  sdrgacs  27178  isdomn3  27192  pm13.196a  27283  refsum2cnlem1  27376  fmul01lt1lem1  27382  stoweidlem14  27431  stoweidlem28  27445  stoweidlem55  27472  stoweid  27480  raaan2  27621  2reu4a  27635  afvfv0bi  27685  frgra3vlem1  27753  frgra3vlem2  27754  3vfriswmgralem  27757  2pthfrgra  27764  4cycl2vnunb  27770  n4cyclfrgra  27771  frgrancvvdeqlemA  27789  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  frgrawopreglem3  27798  frgrawopreglem4  27799  frgraregorufr0  27804  frgraregorufr  27805  sgnn  27870  onfrALTlem5  27971  onfrALTlem3  27973  en3lpVD  28298  onfrALTlem5VD  28338  onfrALTlem3VD  28340  a9e2ndeqVD  28362  a9e2ndeqALT  28385  bnj1109  28495  bnj1542  28566  bnj1253  28724  cvrval2  29389  cvrnbtwn2  29390  cvrnbtwn3  29391  cvlsupr3  29459  hlrelat5N  29515  cvrat4  29557  2at0mat0  29639  dalawlem13  29997  isltrn2N  30234  trlator0  30285  cdleme22b  30455  dochkrshp  31501  dochkrshp4  31504  lcfl6  31615  lclkrlem2x  31645
  Copyright terms: Public domain W3C validator