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

Theorem sneqd 3877
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 3875 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-sn 3866
This theorem is referenced by:  dmsnopss  5299  dmsnsnsn  5305  cnvsng  5313  opswap  5314  ressn  5361  f1osng  5667  fsng  5869  fnressn  5881  fvsng  5899  2nd1st  6608  dfmpt2  6652  cnvf1olem  6659  suppsnop  6693  tpostpos  6754  tfrlem11  6833  ralxpmap  7250  elixpsn  7290  ixpsnf1o  7291  en1b  7365  mapsnen  7375  xpassen  7393  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  wemapweOLD  7917  oef1oOLD  7919  axdc4lem  8612  ttukeylem3  8668  ttukey2g  8673  fpwwe2lem13  8796  fztp  11496  fzsuc2  11498  fseq1p1m1  11517  fseq1m1p1  11518  expval  11850  s1val  12273  s1eq  12274  fsumm1  13203  divalgmod  13592  vdwpc  14023  vdwlem1  14024  vdwlem6  14029  vdwlem7  14030  vdwlem8  14031  cshwsdisj  14107  setsvalg  14179  strle1  14251  imasval  14431  imasaddvallem  14449  imasvscaval  14458  ismri2dad  14557  mreexd  14562  mreexmrid  14563  homaval  14881  setcmon  14937  pwsco2mhm  15480  gsumress  15486  mulgval  15608  symgval  15863  idressubgsymg  15894  gsumzsubmclOLD  16382  gsumzaddlem  16387  gsumzaddlemOLD  16389  pwsgsumOLD  16447  dmdprd  16453  dprdvalOLD  16460  subgdmdprd  16504  dprdsn  16506  dprd2da  16514  dmdprdpr  16521  dprdpr  16522  dpjfval  16527  dpjval  16528  ablfac1eulem  16546  pgpfaclem1  16555  isunit  16682  isdrng  16759  drngprop  16766  isdrngd  16780  drngpropd  16782  issubdrg  16813  lspsnneg  17008  lspsnsub  17009  lmodindp1  17016  islbs  17078  lspsntrim  17100  lbspropd  17101  lspsnvs  17116  lspsneleq  17117  lspfixed  17130  lpival  17248  psrval  17362  zrhrhmb  17783  znval  17807  isobs  17986  frlmval  18014  frlmgsumOLD  18036  frlmlbs  18066  islindf  18082  lindfmm  18097  lsslindf  18100  islindf4  18108  islindf5  18109  mdet0pr  18244  ordtval  18634  ordtcnv  18646  ptval2  19015  dfac14  19032  txdis  19046  xkoptsub  19068  pt1hmeo  19220  xpstopnlem1  19223  xpstopnlem2  19225  tgptsmscls  19565  ustuqtoplem  19655  utopsnneiplem  19663  utopsnneip  19664  utop2nei  19666  utop3cls  19667  pcorev2  20441  pcophtb  20442  pi1grplem  20462  pi1inv  20465  cvsunit  20521  i1f1  21009  i1faddlem  21012  i1fmullem  21013  i1fadd  21014  limcfval  21188  dvnfval  21237  ig1pval  21528  0dgrb  21598  dgreq0  21616  dgrmulc  21622  plyrem  21655  facth  21656  fta1  21658  aaliou2  21690  taylpfval  21714  axlowdimlem15  23024  axlowdim  23029  1pthoncl  23313  2pthlem2  23317  eupath2lem3  23422  drngoi  23716  isdivrngo  23740  0ofval  24009  fcnvgreu  25814  ordtprsval  26201  ordtprsuni  26202  ordtcnvNEW  26203  indval2  26324  sitgval  26565  sseqval  26618  subfacp1lem5  26919  sconpht  26965  sconpht2  26974  sconpi1  26975  cvmliftlem7  27027  cvmliftlem10  27030  cvmlift2lem13  27051  cvmlift3lem9  27063  fprodm1  27323  onint1  28142  finixpnum  28255  ptrest  28266  grpokerinj  28591  isprrngo  28691  dfac11  29257  dfac21  29261  dgrnznn  29334  expgrowth  29451  dfateq12d  29878  otsndisj  29974  otiunsndisj  29975  otiunsndisjX  29976  frgrancvvdeqlem4  30469  frgrancvvdeqlem6  30471  lmod1zr  30741  bnj941  31465  bnj944  31630  bj-projeq  32065  lsatset  32205  lsmsat  32223  islshpat  32232  lflsc0N  32298  lkrfval  32302  ldualset  32340  dvafset  34218  dvaset  34219  dvhfset  34295  dvhset  34296  dibffval  34355  dibfval  34356  dib0  34379  cdlemn4a  34414  dihmeetlem4preN  34521  dihmeetlem13N  34534  dih1dimatlem  34544  dihlsprn  34546  dvh2dim  34660  lpolsetN  34697  lclkrlem2j  34731  lclkrlem2p  34737  lcfrlem21  34778  mapdpglem22  34908  mapdpglem23  34909  mapdpglem26  34913  mapdpglem27  34914  mapdpg  34921  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927  baerlem5amN  34931  baerlem5bmN  34932  baerlem5abmN  34933  mapdindp4  34938  mapdhval  34939  mapdheq  34943  mapdh6aN  34950  hvmapffval  34973  hvmapfval  34974  hvmap1o2  34980  hdmap1fval  35012  hdmap1vallem  35013  hdmap1val  35014  hdmap1eq  35017  hdmap1cbv  35018  hdmap1l6a  35025  hdmap1neglem1N  35043  hdmapfval  35045  hdmap10  35058  hdmaprnlem6N  35072  hgmaprnlem2N  35115
  Copyright terms: Public domain W3C validator