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

Theorem sneqd 4009
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sneqd  |-  ( ph  ->  { A }  =  { B } )

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2  |-  ( ph  ->  A  =  B )
2 sneq 4007 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 17 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438   {csn 3997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-sn 3998
This theorem is referenced by:  otsndisj  4723  otiunsndisj  4724  dmsnopss  5325  dmsnsnsn  5331  cnvsng  5339  opswap  5340  ressn  5389  f1osng  5867  fsng  6076  fsn2g  6077  fnressn  6089  fvsng  6111  2nd1st  6850  dfmpt2  6895  cnvf1olem  6903  suppsnop  6937  tpostpos  6999  tfrlem11  7112  ralxpmap  7527  elixpsn  7567  ixpsnf1o  7568  en1b  7642  mapsnen  7652  xpassen  7670  cantnfp1lem3  8188  axdc4lem  8887  ttukeylem3  8943  ttukey2g  8948  fpwwe2lem13  9069  fztp  11854  fzsuc2  11855  fseq1p1m1  11870  fseq1m1p1  11871  expval  12275  s1val  12735  s1eq  12737  fsumm1  13805  fprodm1  14014  divalgmod  14380  vdwpc  14923  vdwlem1  14924  vdwlem6  14929  vdwlem7  14930  vdwlem8  14931  cshwsdisj  15062  setsvalg  15138  setsidvald  15140  strle1  15214  imasval  15404  imasvalOLD  15405  imasaddvallem  15428  imasvscaval  15437  ismri2dad  15536  mreexd  15541  mreexmrid  15542  homaval  15919  setcmon  15975  funcsetcestrclem1  16032  gsumress  16512  pwsco2mhm  16611  mulgval  16753  symgval  17013  idressubgsymg  17044  gsumzaddlem  17547  dmdprd  17623  subgdmdprd  17660  dprdsn  17662  dprd2da  17668  dmdprdpr  17675  dprdpr  17676  dpjfval  17681  dpjval  17682  ablfac1eulem  17698  pgpfaclem1  17707  isunit  17878  isdrng  17972  drngprop  17979  isdrngd  17993  drngpropd  17995  issubdrg  18026  lspsnneg  18222  lspsnsub  18223  lmodindp1  18230  islbs  18292  lspsntrim  18314  lbspropd  18315  lspsnvs  18330  lspsneleq  18331  lspfixed  18344  lpival  18462  psrval  18579  zrhrhmb  19074  znval  19098  isobs  19275  frlmval  19303  frlmlbs  19347  islindf  19362  lindfmm  19377  lsslindf  19380  islindf4  19388  islindf5  19389  mat1dimmul  19493  mat1dimcrng  19494  mat1rhmval  19496  mat1ric  19504  mat1scmat  19556  mdet0pr  19609  m1detdiag  19614  pmatcoe1fsupp  19717  ordtval  20197  ordtcnv  20209  dissnlocfin  20536  ptval2  20608  dfac14  20625  txdis  20639  xkoptsub  20661  pt1hmeo  20813  xpstopnlem1  20816  xpstopnlem2  20818  tgptsmscls  21156  ustuqtoplem  21246  utopsnneiplem  21254  utopsnneip  21255  utop2nei  21257  utop3cls  21258  pcorev2  22051  pcophtb  22052  pi1grplem  22072  pi1inv  22075  cvsunit  22131  i1f1  22640  i1faddlem  22643  i1fmullem  22644  i1fadd  22645  limcfval  22819  dvnfval  22868  ig1pval  23116  ig1pvalOLD  23122  0dgrb  23192  dgrnznn  23193  dgreq0  23211  dgrmulc  23217  plyrem  23250  facth  23251  fta1  23253  aaliou2  23288  taylpfval  23312  axlowdimlem15  24978  axlowdim  24983  1pthoncl  25314  2pthlem2  25318  eupath2lem3  25699  frgrancvvdeqlem4  25753  frgrancvvdeqlem6  25755  drngoi  26127  isdivrngo  26151  0ofval  26420  fcnvgreu  28271  dispcmp  28688  ordtprsval  28726  ordtprsuni  28727  indval2  28838  sitgval  29167  sseqval  29223  bnj941  29586  bnj944  29751  subfacp1lem5  29909  sconpht  29954  sconpht2  29963  sconpi1  29964  cvmliftlem7  30016  cvmliftlem10  30019  cvmlift2lem13  30040  cvmlift3lem9  30052  msrval  30178  mthmpps  30222  onint1  31108  bj-projeq  31548  finixpnum  31850  ptrest  31859  poimirlem4  31864  poimirlem13  31873  poimirlem14  31874  poimirlem16  31876  poimirlem19  31879  poimirlem26  31886  grpokerinj  32103  isprrngo  32203  lsatset  32481  lsmsat  32499  islshpat  32508  lflsc0N  32574  lkrfval  32578  ldualset  32616  dvafset  34496  dvaset  34497  dvhfset  34573  dvhset  34574  dibffval  34633  dibfval  34634  dib0  34657  cdlemn4a  34692  dihmeetlem4preN  34799  dihmeetlem13N  34812  dih1dimatlem  34822  dihlsprn  34824  dvh2dim  34938  lpolsetN  34975  lclkrlem2j  35009  lclkrlem2p  35015  lcfrlem21  35056  mapdpglem22  35186  mapdpglem23  35187  mapdpglem26  35191  mapdpglem27  35192  mapdpg  35199  baerlem3lem2  35203  baerlem5alem2  35204  baerlem5blem2  35205  baerlem5amN  35209  baerlem5bmN  35210  baerlem5abmN  35211  mapdindp4  35216  mapdhval  35217  mapdheq  35221  mapdh6aN  35228  hvmapffval  35251  hvmapfval  35252  hvmap1o2  35258  hdmap1fval  35290  hdmap1vallem  35291  hdmap1val  35292  hdmap1eq  35295  hdmap1cbv  35296  hdmap1l6a  35303  hdmap1neglem1N  35321  hdmapfval  35323  hdmap10  35336  hdmaprnlem6N  35350  hgmaprnlem2N  35393  dfac11  35846  dfac21  35850  nzprmdif  36532  expgrowth  36548  fzdifsuc2  37378  dfateq12d  38349  iunopeqop  38713  otiunsndisjX  38714  funopsn  38723  funop1  38725  funsneqopsn  38727  lmod1zr  39592
  Copyright terms: Public domain W3C validator