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

Theorem sneqd 3856
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 3854 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1654   {csn 3843
This theorem is referenced by:  dmsnopss  5377  dmsnsnsn  5383  cnvsng  5390  opswap  5391  ressn  5443  f1osng  5751  fsng  5943  fnressn  5954  fvsng  5963  2nd1st  6428  dfmpt2  6473  cnvf1olem  6480  tpostpos  6535  snriota  6616  tfrlem11  6685  elixpsn  7137  ixpsnf1o  7138  en1b  7211  mapsnen  7220  xpassen  7238  cantnfp1lem3  7672  wemapwe  7690  oef1o  7691  axdc4lem  8373  ttukeylem3  8429  ttukey2g  8434  fpwwe2lem13  8555  fztp  11140  fzsuc2  11142  fseq1p1m1  11160  fseq1m1p1  11161  expval  11422  s1val  11790  s1eq  11791  fsumm1  12575  divalgmod  12964  vdwpc  13386  vdwlem1  13387  vdwlem6  13392  vdwlem7  13393  vdwlem8  13394  setsvalg  13530  strle1  13598  imasval  13775  imasaddvallem  13792  imasvscaval  13801  ismri2dad  13900  mreexd  13905  mreexmrid  13906  homaval  14224  setcmon  14280  pwsco2mhm  14808  gsumress  14815  mulgval  14930  symgval  15132  gsumzsubmcl  15561  gsumzaddlem  15564  pwsgsum  15591  dmdprd  15597  dprdval  15599  subgdmdprd  15630  dprdsn  15632  dprd2da  15638  dmdprdpr  15645  dprdpr  15646  dpjfval  15651  dpjval  15652  ablfac1eulem  15668  pgpfaclem1  15677  isunit  15800  isdrng  15877  drngprop  15884  isdrngd  15898  drngpropd  15900  issubdrg  15931  lspsnneg  16120  lspsnsub  16121  lmodindp1  16128  islbs  16186  lspsntrim  16208  lbspropd  16209  lspsnvs  16224  lspsneleq  16225  lspfixed  16238  lpival  16354  psrval  16467  mplval  16530  ressmplbas2  16556  mplbaspropd  16668  zrhrhmb  16830  znval  16854  isobs  16985  ordtval  17291  ordtcnv  17303  ptval2  17671  dfac14  17688  txdis  17702  xkoptsub  17724  pt1hmeo  17876  xpstopnlem1  17879  xpstopnlem2  17881  tgptsmscls  18217  ustuqtoplem  18307  utopsnneiplem  18315  utopsnneip  18316  utop2nei  18318  utop3cls  18319  pcorev2  19091  pcophtb  19092  pi1grplem  19112  pi1inv  19115  i1f1  19618  i1faddlem  19621  i1fmullem  19622  i1fadd  19623  limcfval  19797  dvnfval  19846  mdegfval  20023  mdegpropd  20045  ig1pval  20133  0dgrb  20203  dgreq0  20221  dgrmulc  20227  plyrem  20260  facth  20261  fta1  20263  aaliou2  20295  taylpfval  20319  1pthoncl  21630  2pthlem2  21634  eupath2lem3  21739  drngoi  22033  isdivrngo  22057  0ofval  22326  indval2  24447  sitgval  24682  subfacp1lem5  24905  sconpht  24951  sconpht2  24960  sconpi1  24961  cvmliftlem7  25013  cvmliftlem10  25016  cvmlift2lem13  25037  cvmlift3lem9  25049  fprodm1  25325  axlowdimlem15  25930  axlowdim  25935  onint1  26234  grpokerinj  26602  isprrngo  26702  ralxpmap  26854  dfac11  27249  dfac21  27253  frlmval  27305  frlmgsum  27321  uvcresum  27331  frlmlbs  27338  frlmup1  27339  islindf  27371  lindfmm  27386  lsslindf  27389  islindf4  27397  islindf5  27398  dgrnznn  27429  expgrowth  27641  dfateq12d  28081  otsndisj  28178  otiunsndisj  28179  otiunsndisjX  28180  cshwsdisj  28417  frgrancvvdeqlem4  28594  frgrancvvdeqlem6  28596  bnj941  29317  bnj944  29483  lsatset  29962  lsmsat  29980  islshpat  29989  lflsc0N  30055  lkrfval  30059  ldualset  30097  dvafset  31975  dvaset  31976  dvhfset  32052  dvhset  32053  dibffval  32112  dibfval  32113  dib0  32136  cdlemn4a  32171  dihmeetlem4preN  32278  dihmeetlem13N  32291  dih1dimatlem  32301  dihlsprn  32303  dvh2dim  32417  lpolsetN  32454  lclkrlem2j  32488  lclkrlem2p  32494  lcfrlem21  32535  mapdpglem22  32665  mapdpglem23  32666  mapdpglem26  32670  mapdpglem27  32671  mapdpg  32678  baerlem3lem2  32682  baerlem5alem2  32683  baerlem5blem2  32684  baerlem5amN  32688  baerlem5bmN  32689  baerlem5abmN  32690  mapdindp4  32695  mapdhval  32696  mapdheq  32700  mapdh6aN  32707  hvmapffval  32730  hvmapfval  32731  hvmap1o2  32737  hdmap1fval  32769  hdmap1vallem  32770  hdmap1val  32771  hdmap1eq  32774  hdmap1cbv  32775  hdmap1l6a  32782  hdmap1neglem1N  32800  hdmapfval  32802  hdmap10  32815  hdmaprnlem6N  32829  hgmaprnlem2N  32872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-sn 3849
  Copyright terms: Public domain W3C validator