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

Definition df-ne 2640
Description: Define inequality. (Contributed by NM, 26-May-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 2638 . 2  wff  A  =/= 
B
41, 2wceq 1383 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 184 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff setvar class
This definition is referenced by:  neii  2642  neir  2643  nne  2644  neneqd  2645  neqned  2646  exmidne  2648  exmidneOLD  2649  eqneqall  2650  nonconneOLD  2652  necon2bd  2658  necon1adOLD  2660  necon1bd  2661  necon3d  2667  necon2d  2669  necon1aiOLD  2675  necon1bi  2676  necon1i  2685  necon3abid  2689  necon1abidOLD  2692  necon1bbid  2693  necon4abidOLD  2695  necon2abidOLD  2698  necon2bbidOLD  2700  necon3bid  2701  necon3abii  2703  necon1abiiOLD  2706  necon1bbiiOLD  2708  necon3bii  2711  neeq1OLD  2725  neeq2OLD  2727  pm2.61iineOLD  2766  neor  2767  neanior  2768  neorian  2770  nfne  2774  nfned  2775  nabbi  2776  nabbiOLD  2777  dfpss2  3574  neq0  3781  ifnefalse  3938  snnzb  4079  raldifsni  4145  eqsn  4176  opthpr  4193  unissint  4296  iununi  4400  disji2  4424  opthneg  4716  ord0eln0  4922  unizlim  4984  frsn  5060  xpcan  5433  xpcan2  5434  xpima  5439  unixpid  5532  dff14a  6162  mpt2difsnif  6380  orduniorsuc  6650  dflim3  6667  tfindsg  6680  nn0suc  6709  findsg  6712  suppvalbr  6907  tz7.49  7112  oevn0  7167  php  7703  1sdom  7724  fimaxg  7769  fiint  7799  wemapsolem  7978  card2on  7983  brwdomn0  7998  domwdom  8003  rankxplim2  8301  rankxplim3  8302  carden2a  8350  dfackm  8549  fin23lem14  8716  fin1a2lem12  8794  axcc2lem  8819  ac6num  8862  zorn2lem4  8882  zorn2lem7  8885  brdom3  8909  iundom2g  8918  r1tskina  9163  1re  9598  ltlen  9689  uzm1  11122  xrnemnf  11339  xrnepnf  11340  ioo0  11565  ico0  11586  ioc0  11587  icc0  11588  elfznelfzo  11897  elfznelfzob  11898  injresinjlem  11907  fleqceilz  11963  fsuppmapnn0fiubex  12080  sq01  12270  hash1snb  12461  hashgt12el  12463  hashgt12el2  12464  hashfun  12477  hash2prde  12498  hash2prd  12500  hashge2el2dif  12503  swrdccatin1  12690  repswcshw  12762  cshw1  12772  incexc2  13632  sqrt2irr  13964  divalglem8  14040  ndvdssub  14047  algcvgblem  14188  isprm2lem  14206  isprm3  14208  isprm4  14209  ramcl2lem  14509  cshwshashlem1  14562  cshwshash  14571  isnsgrp  15894  isnmnd  15903  sgrp2nmndlem3  16022  sgrp2rid2  16023  sgrp2nmndlem5  16026  symg2bas  16402  symgextf  16421  symgextfv  16422  odlem1  16538  gexlem1  16578  dprdfeq0  17041  dprdfeq0OLD  17048  isnirred  17328  isirred2  17329  drngmul0or  17396  drngmuleq0  17398  lvecvs0or  17733  lvecvscan  17736  isnzr2  17890  isdomn2  17927  cply1mul  18314  gsummoncoe1  18325  domnchr  18547  psgndiflemB  18614  dmatmul  18977  mulmarep1gsum1  19053  mulmarep1gsum2  19054  mdetdiag  19079  mdetunilem8  19099  mdetunilem9  19100  madurid  19124  mp2pm2mplem4  19288  fvmptnn04if  19328  fvmptnn04ifb  19330  elcls  19552  opnnei  19599  ist0-3  19824  ist1-2  19826  dfcon2  19898  cnconn  19901  pthaus  20117  xkohaus  20132  hausflim  20460  cldsubg  20587  bcth  21746  ioorinv  21963  tdeglem4  22436  fta1b  22548  plydivex  22671  plyexmo  22687  aalioulem3  22708  dvradcnv  22794  logtayllem  23018  logtayl  23019  cxpcl  23033  recxpcl  23034  logrec  23129  isosctrlem2  23131  efrlim  23277  muval2  23386  musum  23445  dchrelbas2  23490  dchrelbas4  23496  dchrfi  23508  dchrptlem3  23519  dchrsum2  23521  sumdchr2  23523  lgscllem  23556  2sqb  23631  dchrvmasumiflem2  23665  rpvmasum2  23675  padicabv  23793  padicabvf  23794  padicabvcxp  23795  tglowdim1i  23870  tgbtwnconn1  23940  colline  24008  colmid  24043  lmimid  24137  lmiisolem  24139  brbtwn2  24186  colinearalg  24191  axlowdimlem6  24228  axlowdimlem14  24236  axcontlem12  24256  usgra2edg1  24361  nbgranself  24412  nb3graprlem1  24429  uvtx01vtx  24470  wlkdvspthlem  24587  usgrcyclnl1  24618  usgrcyclnl2  24619  constr3trllem2  24629  wwlknext  24702  clwlkisclwwlklem2a4  24762  clwwisshclwwn  24786  clwlknclwlkdifs  24938  eupath2lem1  24955  frgra3vlem1  24978  frgra3vlem2  24979  3vfriswmgralem  24982  2pthfrgra  24989  4cycl2vnunb  24995  n4cyclfrgra  24996  frgrancvvdeqlemA  25015  frgrancvvdeqlemB  25016  frgrancvvdeqlemC  25017  frgraregorufr0  25030  frgraregorufr  25031  numclwwlk3lem  25086  frgrareg  25095  frgraregord013  25096  ismgmOLD  25300  nvmul0or  25525  nmogtmnf  25663  hvmul0or  25920  hvmulcan  25967  hvmulcan2  25968  hiidge0  25993  bcsiALT  26074  shne0i  26344  nonbooli  26547  nmopgtmnf  26765  unopbd  26912  nmcfnlbi  26949  nmopcoi  26992  chirredi  27291  mdsymlem5  27304  sumdmdlem2  27316  disji2f  27416  imadifxp  27436  2sqcoprm  27613  sgn3da  28458  plymulx  28483  subfacp1lem6  28607  cvmsdisj  28693  wfrlem16  29334  sltval2  29392  sltres  29400  nodenselem4  29420  nodenselem5  29421  nodenselem7  29423  nobndup  29436  nobnddown  29437  nofulllem5  29442  btwnconn1lem13  29725  lineunray  29773  rankeq1o  29804  ordtoplem  29876  itg2addnclem3  30044  itgaddnclem2  30050  elicc3  30111  nn0prpw  30117  fdc  30214  prtlem90  30574  fphpd  30726  jm2.23  30914  sdrgacs  31126  isdomn3  31140  lcmcllem  31178  pm13.196a  31275  cncfiooicclem1  31650  iblcncfioo  31731  stoweidlem28  31764  raaan2  32134  2reu4a  32148  afvfv0bi  32191  pr1eqbg  32251  2f1fvneq  32261  2ffzoeq  32295  usg2edgneu  32366  copisnmnd  32450  fdmdifeqresdif  32799  pgrpgt2nabl  32827  islindeps  32924  lincext1  32925  lindslinindsimp2lem5  32933  snlindsntor  32942  ldepslinc  32980  onfrALTlem5  33182  onfrALTlem3  33184  en3lpVD  33513  onfrALTlem5VD  33553  onfrALTlem3VD  33555  ax6e2ndeqVD  33577  ax6e2ndeqALT  33599  isosctrlem1ALT  33602  bnj1109  33713  bnj1542  33783  bnj1253  33941  cvrval2  34874  cvrnbtwn2  34875  cvrnbtwn3  34876  cvlsupr3  34944  cvrat4  35042  2at0mat0  35124  dalawlem13  35482  isltrn2N  35719  trlator0  35771  cdleme22b  35942  dochkrshp  36988  dochkrshp4  36991  lcfl6  37102  lclkrlem2x  37132  xptrrel  37603
  Copyright terms: Public domain W3C validator