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

Theorem sneqd 4041
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1
Assertion
Ref Expression
sneqd

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2
2 sneq 4039 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {csn 4029
This theorem is referenced by:  otsndisj  4757  otiunsndisj  4758  dmsnopss  5485  dmsnsnsn  5491  cnvsng  5499  opswap  5500  ressn  5548  f1osng  5859  fsng  6070  fnressn  6083  fvsng  6105  2nd1st  6845  dfmpt2  6890  cnvf1olem  6898  suppsnop  6932  tpostpos  6994  tfrlem11  7076  ralxpmap  7488  elixpsn  7528  ixpsnf1o  7529  en1b  7603  mapsnen  7613  xpassen  7631  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  wemapweOLD  8161  oef1oOLD  8163  axdc4lem  8856  ttukeylem3  8912  ttukey2g  8917  fpwwe2lem13  9041  fztp  11765  fzsuc2  11766  fseq1p1m1  11781  fseq1m1p1  11782  expval  12168  s1val  12610  s1eq  12612  fsumm1  13566  fprodm1  13771  divalgmod  14064  vdwpc  14498  vdwlem1  14499  vdwlem6  14504  vdwlem7  14505  vdwlem8  14506  cshwsdisj  14583  setsvalg  14655  strle1  14728  imasval  14908  imasaddvallem  14926  imasvscaval  14935  ismri2dad  15034  mreexd  15039  mreexmrid  15040  homaval  15358  setcmon  15414  gsumress  15903  pwsco2mhm  16002  mulgval  16144  symgval  16404  idressubgsymg  16435  gsumzsubmclOLD  16929  gsumzaddlem  16934  gsumzaddlemOLD  16936  pwsgsumOLD  17010  dmdprd  17029  dprdvalOLD  17036  subgdmdprd  17081  dprdsn  17083  dprd2da  17091  dmdprdpr  17098  dprdpr  17099  dpjfval  17104  dpjval  17105  ablfac1eulem  17123  pgpfaclem1  17132  isunit  17306  isdrng  17400  drngprop  17407  isdrngd  17421  drngpropd  17423  issubdrg  17454  lspsnneg  17652  lspsnsub  17653  lmodindp1  17660  islbs  17722  lspsntrim  17744  lbspropd  17745  lspsnvs  17760  lspsneleq  17761  lspfixed  17774  lpival  17893  psrval  18011  zrhrhmb  18548  znval  18572  isobs  18751  frlmval  18779  frlmgsumOLD  18801  frlmlbs  18831  islindf  18847  lindfmm  18862  lsslindf  18865  islindf4  18873  islindf5  18874  mat1dimmul  18978  mat1dimcrng  18979  mat1rhmval  18981  mat1ric  18989  mat1scmat  19041  mdet0pr  19094  m1detdiag  19099  pmatcoe1fsupp  19202  ordtval  19690  ordtcnv  19702  dissnlocfin  20030  ptval2  20102  dfac14  20119  txdis  20133  xkoptsub  20155  pt1hmeo  20307  xpstopnlem1  20310  xpstopnlem2  20312  tgptsmscls  20652  ustuqtoplem  20742  utopsnneiplem  20750  utopsnneip  20751  utop2nei  20753  utop3cls  20754  pcorev2  21528  pcophtb  21529  pi1grplem  21549  pi1inv  21552  cvsunit  21608  i1f1  22097  i1faddlem  22100  i1fmullem  22101  i1fadd  22102  limcfval  22276  dvnfval  22325  ig1pval  22573  0dgrb  22643  dgrnznn  22644  dgreq0  22662  dgrmulc  22668  plyrem  22701  facth  22702  fta1  22704  aaliou2  22736  taylpfval  22760  axlowdimlem15  24259  axlowdim  24264  1pthoncl  24594  2pthlem2  24598  eupath2lem3  24979  frgrancvvdeqlem4  25033  frgrancvvdeqlem6  25035  drngoi  25409  isdivrngo  25433  0ofval  25702  fcnvgreu  27514  dispcmp  27862  ordtprsval  27900  ordtprsuni  27901  indval2  28028  sitgval  28274  sseqval  28327  subfacp1lem5  28628  sconpht  28674  sconpht2  28683  sconpi1  28684  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem13  28760  cvmlift3lem9  28772  msrval  28898  mthmpps  28942  onint1  29914  finixpnum  30038  ptrest  30048  grpokerinj  30347  isprrngo  30447  dfac11  31008  dfac21  31012  nzprmdif  31224  expgrowth  31240  fzdifsuc2  31512  dfateq12d  32214  otiunsndisjX  32301  setsidvald  32557  funcsetcestrclem1  32660  lmod1zr  33094  bnj941  33831  bnj944  33996  bj-projeq  34550  lsatset  34715  lsmsat  34733  islshpat  34742  lflsc0N  34808  lkrfval  34812  ldualset  34850  dvafset  36730  dvaset  36731  dvhfset  36807  dvhset  36808  dibffval  36867  dibfval  36868  dib0  36891  cdlemn4a  36926  dihmeetlem4preN  37033  dihmeetlem13N  37046  dih1dimatlem  37056  dihlsprn  37058  dvh2dim  37172  lpolsetN  37209  lclkrlem2j  37243  lclkrlem2p  37249  lcfrlem21  37290  mapdpglem22  37420  mapdpglem23  37421  mapdpglem26  37425  mapdpglem27  37426  mapdpg  37433  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  baerlem5amN  37443  baerlem5bmN  37444  baerlem5abmN  37445  mapdindp4  37450  mapdhval  37451  mapdheq  37455  mapdh6aN  37462  hvmapffval  37485  hvmapfval  37486  hvmap1o2  37492  hdmap1fval  37524  hdmap1vallem  37525  hdmap1val  37526  hdmap1eq  37529  hdmap1cbv  37530  hdmap1l6a  37537  hdmap1neglem1N  37555  hdmapfval  37557  hdmap10  37570  hdmaprnlem6N  37584  hgmaprnlem2N  37627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4030
  Copyright terms: Public domain W3C validator