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

Theorem sneqd 3791
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 3789 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   {csn 3778
This theorem is referenced by:  dmsnopss  5305  dmsnsnsn  5311  cnvsng  5318  opswap  5319  ressn  5371  f1osng  5679  fsng  5870  fnressn  5881  fvsng  5890  2nd1st  6355  dfmpt2  6400  cnvf1olem  6407  tpostpos  6462  snriota  6543  tfrlem11  6612  elixpsn  7064  ixpsnf1o  7065  en1b  7138  mapsnen  7147  xpassen  7165  cantnfp1lem3  7596  wemapwe  7614  oef1o  7615  axdc4lem  8295  ttukeylem3  8351  ttukey2g  8356  fpwwe2lem13  8477  fztp  11062  fzsuc2  11064  fseq1p1m1  11081  fseq1m1p1  11082  expval  11343  s1val  11711  s1eq  11712  fsumm1  12496  divalgmod  12885  vdwpc  13307  vdwlem1  13308  vdwlem6  13313  vdwlem7  13314  vdwlem8  13315  setsvalg  13451  strle1  13519  imasval  13696  imasaddvallem  13713  imasvscaval  13722  ismri2dad  13821  mreexd  13826  mreexmrid  13827  homaval  14145  setcmon  14201  pwsco2mhm  14729  gsumress  14736  mulgval  14851  symgval  15053  gsumzsubmcl  15482  gsumzaddlem  15485  pwsgsum  15512  dmdprd  15518  dprdval  15520  subgdmdprd  15551  dprdsn  15553  dprd2da  15559  dmdprdpr  15566  dprdpr  15567  dpjfval  15572  dpjval  15573  ablfac1eulem  15589  pgpfaclem1  15598  isunit  15721  isdrng  15798  drngprop  15805  isdrngd  15819  drngpropd  15821  issubdrg  15852  lspsnneg  16041  lspsnsub  16042  lmodindp1  16049  islbs  16107  lspsntrim  16129  lbspropd  16130  lspsnvs  16145  lspsneleq  16146  lspfixed  16159  lpival  16275  psrval  16388  mplval  16451  ressmplbas2  16477  mplbaspropd  16589  zrhrhmb  16751  znval  16775  isobs  16906  ordtval  17211  ordtcnv  17223  ptval2  17590  dfac14  17607  txdis  17621  xkoptsub  17643  pt1hmeo  17795  xpstopnlem1  17798  xpstopnlem2  17800  tgptsmscls  18136  ustuqtoplem  18226  utopsnneiplem  18234  utopsnneip  18235  utop2nei  18237  utop3cls  18238  pcorev2  19010  pcophtb  19011  pi1grplem  19031  pi1inv  19034  i1f1  19539  i1faddlem  19542  i1fmullem  19543  i1fadd  19544  limcfval  19716  dvnfval  19765  mdegfval  19942  mdegpropd  19964  ig1pval  20052  0dgrb  20122  dgreq0  20140  dgrmulc  20146  plyrem  20179  facth  20180  fta1  20182  aaliou2  20214  taylpfval  20238  1pthoncl  21549  2pthlem2  21553  eupath2lem3  21658  drngoi  21952  isdivrngo  21976  0ofval  22245  indval2  24369  sitgval  24604  subfacp1lem5  24827  sconpht  24873  sconpht2  24882  sconpi1  24883  cvmliftlem7  24935  cvmliftlem10  24938  cvmlift2lem13  24959  cvmlift3lem9  24971  fprodm1  25247  axlowdimlem15  25803  axlowdim  25808  onint1  26107  grpokerinj  26454  isprrngo  26554  ralxpmap  26636  dfac11  27032  dfac21  27036  frlmval  27088  frlmgsum  27104  uvcresum  27114  frlmlbs  27121  frlmup1  27122  islindf  27154  lindfmm  27169  lsslindf  27172  islindf4  27180  islindf5  27181  dgrnznn  27212  expgrowth  27424  dfateq12d  27864  otsndisj  27957  otiunsndisj  27958  otiunsndisjX  27959  frgrancvvdeqlem4  28140  frgrancvvdeqlem6  28142  bnj941  28853  bnj944  29019  lsatset  29477  lsmsat  29495  islshpat  29504  lflsc0N  29570  lkrfval  29574  ldualset  29612  dvafset  31490  dvaset  31491  dvhfset  31567  dvhset  31568  dibffval  31627  dibfval  31628  dib0  31651  cdlemn4a  31686  dihmeetlem4preN  31793  dihmeetlem13N  31806  dih1dimatlem  31816  dihlsprn  31818  dvh2dim  31932  lpolsetN  31969  lclkrlem2j  32003  lclkrlem2p  32009  lcfrlem21  32050  mapdpglem22  32180  mapdpglem23  32181  mapdpglem26  32185  mapdpglem27  32186  mapdpg  32193  baerlem3lem2  32197  baerlem5alem2  32198  baerlem5blem2  32199  baerlem5amN  32203  baerlem5bmN  32204  baerlem5abmN  32205  mapdindp4  32210  mapdhval  32211  mapdheq  32215  mapdh6aN  32222  hvmapffval  32245  hvmapfval  32246  hvmap1o2  32252  hdmap1fval  32284  hdmap1vallem  32285  hdmap1val  32286  hdmap1eq  32289  hdmap1cbv  32290  hdmap1l6a  32297  hdmap1neglem1N  32315  hdmapfval  32317  hdmap10  32330  hdmaprnlem6N  32344  hgmaprnlem2N  32387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-sn 3784
  Copyright terms: Public domain W3C validator