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

Definition df-ne 2569
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 2567 . 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  2571  exmidne  2573  nonconne  2574  neeq1  2575  neeq2  2576  neneqd  2583  necon3abii  2597  necon3bii  2599  necon3abid  2600  necon3bid  2602  necon3d  2605  necon1ai  2609  necon1i  2611  necon2bd  2616  necon2d  2617  necon1abii  2618  necon1bbii  2619  necon1abid  2620  necon1bbid  2621  necon2abid  2624  necon2bbid  2625  necon4abid  2631  necon1ad  2634  neor  2651  neanior  2652  neorian  2654  nemtbir  2655  nfne  2658  nfned  2659  dfpss2  3392  neq0  3598  ifnefalse  3707  eqsn  3920  snsssn  3927  opthpr  3936  prnebg  3939  unissint  4034  iununi  4135  disji2  4159  ord0eln0  4595  nsuceq0  4621  unizlim  4657  orduniorsuc  4769  dflim3  4786  tfindsg  4799  nn0suc  4828  findsg  4831  frsn  4907  xpcan  5264  xpcan2  5265  xpima  5272  unixpid  5363  0neqopab  6078  bropopvvv  6385  tz7.49  6661  oevn0  6718  2dom  7138  map2xp  7236  php  7250  1sdom  7270  fimaxg  7313  fiint  7342  wemapso2lem  7475  card2on  7478  brwdomn0  7493  domwdom  7498  rankxplim2  7760  rankxplim3  7761  carden2a  7809  pm54.43lem  7842  dfackm  8002  fin23lem14  8169  fin1a2lem12  8247  axcc2lem  8272  ac6num  8315  zorn2lem4  8335  zorn2lem7  8338  brdom3  8362  iundom2g  8371  canthp1lem2  8484  r1tskina  8613  ax1ne0  8991  1re  9046  ltlen  9131  ine0  9425  recgt0ii  9872  inelr  9946  nnunb  10173  uzm1  10472  xrnemnf  10674  xrnepnf  10675  xrltnr  10676  pnfnlt  10681  nltmnf  10682  xrltlen  10695  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  fzm1  11082  elfznelfzo  11147  elfznelfzob  11148  injresinjlem  11154  sq01  11456  hash1snb  11636  hashgt12el  11637  hashgt12el2  11638  hash2prde  11643  hashfun  11655  incexc2  12573  sqr2irr  12803  divalglem8  12875  ndvdssub  12882  algcvgblem  13023  isprm2lem  13041  isprm3  13043  isprm4  13044  ramcl2lem  13332  xpsfrnel2  13745  setcepi  14198  odlem1  15128  gexlem1  15168  dprdfeq0  15535  isnirred  15760  isirred2  15761  drngmul0or  15811  drngmuleq0  15813  lvecvs0or  16135  lvecvscan  16138  lspsncv0  16173  isnzr2  16289  isdomn2  16314  domnchr  16768  elcls  17092  opnnei  17139  ist0-3  17363  ist1-2  17365  dfcon2  17435  cnconn  17438  pthaus  17623  xkohaus  17638  trfbas  17829  fbunfip  17854  trfil2  17872  hausflim  17966  cldsubg  18093  bcth  19235  iundisj2  19396  ioorinv  19421  tdeglem4  19936  fta1b  20045  plydivex  20167  vieta1lem2  20181  plyexmo  20183  aalioulem3  20204  dvradcnv  20290  sinhalfpilem  20327  coseq1  20383  logtayllem  20503  logtayl  20504  cxpcl  20518  recxpcl  20519  logrec  20614  isosctrlem2  20616  efrlim  20761  muval2  20870  musum  20929  dchrelbas2  20974  dchrelbas4  20980  dchrfi  20992  dchrptlem3  21003  dchrsum2  21005  sumdchr2  21007  lgscllem  21040  2sqb  21115  dchrvmasumiflem2  21149  rpvmasum2  21159  padicabv  21277  padicabvf  21278  padicabvcxp  21279  usgraedgprv  21349  usgra2edg  21355  usgra2edg1  21356  nbgranself  21399  nb3graprlem1  21413  uvtx01vtx  21454  2trllemA  21503  wlkntrllem3  21514  2pthon  21555  2pthon3v  21557  wlkdvspthlem  21560  usgrcyclnl1  21580  usgrcyclnl2  21581  constr3trllem2  21591  4cycl4dv  21607  eupath2lem1  21652  ismgm  21861  vcoprne  22011  nvmul0or  22086  nmogtmnf  22224  hvmul0or  22480  hvmulcan  22527  hvmulcan2  22528  hiidge0  22553  bcsiALT  22634  norm1exi  22705  shne0i  22903  nonbooli  23106  nmopgtmnf  23324  unopbd  23471  nmcfnlbi  23508  nmopcoi  23551  largei  23723  chirredi  23850  mdsymlem5  23863  sumdmdlem2  23875  disji2f  23972  iundisj2f  23983  imadifxp  23991  iundisj2fi  24106  ind1a  24371  ballotlemii  24714  subfacp1lem6  24824  cvmsdisj  24910  cvmscld  24913  pm2.61iine  25139  dfrdg2  25366  wfrlem16  25485  sltval2  25524  nosgnn0  25526  nosgnn0i  25527  sltintdifex  25531  sltres  25532  sltsolem1  25536  nodenselem4  25552  nodenselem5  25553  nodenselem7  25555  nobndup  25568  nobnddown  25569  nofulllem5  25574  dfrdg4  25703  brbtwn2  25748  colinearalg  25753  axlowdimlem6  25790  axlowdimlem13  25797  axlowdimlem14  25798  axlowdim1  25802  axcontlem12  25818  btwnconn1lem13  25937  lineunray  25985  rankeq1o  26016  ordtoplem  26089  itg2addnclem3  26157  itgaddnclem2  26163  elicc3  26210  nn0prpw  26216  fdc  26339  prtlem90  26596  raldifsni  26624  cmpfiiin  26641  0dioph  26727  fphpd  26767  jm2.23  26957  wepwsolem  27006  uvcvv0  27107  sdrgacs  27377  isdomn3  27391  pm13.196a  27482  refsum2cnlem1  27575  fmul01lt1lem1  27581  stoweidlem14  27630  stoweidlem28  27644  stoweidlem55  27671  stoweid  27679  raaan2  27820  2reu4a  27834  afvfv0bi  27883  eqneqall  27939  pr1eqbg  27944  2f1fvneq  27958  dff14a  27959  euhash1  27998  swrdccatin1  28016  swrdccatin12b  28027  swrdccatin12c  28028  frgra3vlem1  28104  frgra3vlem2  28105  3vfriswmgralem  28108  2pthfrgra  28115  4cycl2vnunb  28121  n4cyclfrgra  28122  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrawopreglem3  28149  frgrawopreglem4  28150  frgraregorufr0  28155  frgraregorufr  28156  usg2spot2nb  28168  sgnn  28238  onfrALTlem5  28339  onfrALTlem3  28341  en3lpVD  28666  onfrALTlem5VD  28706  onfrALTlem3VD  28708  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj1109  28863  bnj1542  28934  bnj1253  29092  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn3  29759  cvlsupr3  29827  hlrelat5N  29883  cvrat4  29925  2at0mat0  30007  dalawlem13  30365  isltrn2N  30602  trlator0  30653  cdleme22b  30823  dochkrshp  31869  dochkrshp4  31872  lcfl6  31983  lclkrlem2x  32013
  Copyright terms: Public domain W3C validator