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

Theorem sneqd 3729
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 3727 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 15 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   {csn 3716
This theorem is referenced by:  dmsnopss  5227  dmsnsnsn  5233  cnvsng  5240  opswap  5241  ressn  5293  f1osng  5597  fsng  5780  fnressn  5789  fvsng  5798  2nd1st  6252  dfmpt2  6296  cnvf1olem  6303  tpostpos  6341  snriota  6422  tfrlem11  6491  elixpsn  6943  ixpsnf1o  6944  en1b  7017  mapsnen  7026  xpassen  7044  cantnfp1lem3  7472  wemapwe  7490  oef1o  7491  axdc4lem  8171  ttukeylem3  8228  ttukey2g  8233  fpwwe2lem13  8354  fztp  10933  fzsuc2  10934  fseq1p1m1  10949  fseq1m1p1  10950  expval  11199  s1val  11534  s1eq  11535  fsumm1  12313  divalgmod  12702  vdwpc  13124  vdwlem1  13125  vdwlem6  13130  vdwlem7  13131  vdwlem8  13132  setsvalg  13268  strle1  13336  imasval  13513  imasaddvallem  13530  imasvscaval  13539  ismri2dad  13638  mreexd  13643  mreexmrid  13644  homaval  13962  setcmon  14018  pwsco2mhm  14546  gsumress  14553  mulgval  14668  symgval  14870  gsumzsubmcl  15299  gsumzaddlem  15302  pwsgsum  15329  dmdprd  15335  dprdval  15337  subgdmdprd  15368  dprdsn  15370  dprd2da  15376  dmdprdpr  15383  dprdpr  15384  dpjfval  15389  dpjval  15390  ablfac1eulem  15406  pgpfaclem1  15415  isunit  15538  isdrng  15615  drngprop  15622  isdrngd  15636  drngpropd  15638  issubdrg  15669  lspsnneg  15862  lspsnsub  15863  lmodindp1  15870  islbs  15928  lspsntrim  15950  lbspropd  15951  lspsnvs  15966  lspsneleq  15967  lspfixed  15980  lpival  16096  psrval  16209  mplval  16272  ressmplbas2  16298  mplbaspropd  16413  zrhrhmb  16571  znval  16595  isobs  16726  ordtval  17025  ordtcnv  17037  ptval2  17402  dfac14  17418  txdis  17432  xkoptsub  17454  pt1hmeo  17603  xpstopnlem1  17606  xpstopnlem2  17608  tgptsmscls  17934  pcorev2  18630  pcophtb  18631  pi1grplem  18651  pi1inv  18654  i1f1  19149  i1faddlem  19152  i1fmullem  19153  i1fadd  19154  limcfval  19326  dvnfval  19375  mdegfval  19552  mdegpropd  19574  ig1pval  19662  0dgrb  19732  dgreq0  19750  dgrmulc  19756  plyrem  19789  facth  19790  fta1  19792  aaliou2  19824  taylpfval  19848  drngoi  21186  isdivrngo  21210  0ofval  21479  ustuqtoplem  23543  utopsnneiplem  23551  indval2  23678  subfacp1lem5  24119  sconpht  24164  sconpht2  24173  sconpi1  24174  cvmliftlem7  24226  cvmliftlem10  24229  cvmlift2lem13  24250  cvmlift3lem9  24262  eupath2lem3  24307  fprodm1  24591  axlowdimlem15  25143  axlowdim  25148  onint1  25447  grpokerinj  25898  isprrngo  25998  ralxpmap  26084  dfac11  26483  dfac21  26487  frlmval  26539  frlmgsum  26555  uvcresum  26565  frlmlbs  26572  frlmup1  26573  islindf  26605  lindfmm  26620  lsslindf  26623  islindf4  26631  islindf5  26632  dgrnznn  26663  expgrowth  26875  dfateq12d  27317  1pthoncl  27728  2pthonlem2  27736  frgrancvvdeqlem4  27866  frgrancvvdeqlem6  27868  bnj941  28566  bnj944  28732  lsatset  29249  lsmsat  29267  islshpat  29276  lflsc0N  29342  lkrfval  29346  ldualset  29384  dvafset  31262  dvaset  31263  dvhfset  31339  dvhset  31340  dibffval  31399  dibfval  31400  dib0  31423  cdlemn4a  31458  dihmeetlem4preN  31565  dihmeetlem13N  31578  dih1dimatlem  31588  dihlsprn  31590  dvh2dim  31704  lpolsetN  31741  lclkrlem2j  31775  lclkrlem2p  31781  lcfrlem21  31822  mapdpglem22  31952  mapdpglem23  31953  mapdpglem26  31957  mapdpglem27  31958  mapdpg  31965  baerlem3lem2  31969  baerlem5alem2  31970  baerlem5blem2  31971  baerlem5amN  31975  baerlem5bmN  31976  baerlem5abmN  31977  mapdindp4  31982  mapdhval  31983  mapdheq  31987  mapdh6aN  31994  hvmapffval  32017  hvmapfval  32018  hvmap1o2  32024  hdmap1fval  32056  hdmap1vallem  32057  hdmap1val  32058  hdmap1eq  32061  hdmap1cbv  32062  hdmap1l6a  32069  hdmap1neglem1N  32087  hdmapfval  32089  hdmap10  32102  hdmaprnlem6N  32116  hgmaprnlem2N  32159
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-sn 3722
  Copyright terms: Public domain W3C validator