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

Theorem sneqd 3827
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 3825 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {csn 3814
This theorem is referenced by:  dmsnopss  5342  dmsnsnsn  5348  cnvsng  5355  opswap  5356  ressn  5408  f1osng  5716  fsng  5907  fnressn  5918  fvsng  5927  2nd1st  6392  dfmpt2  6437  cnvf1olem  6444  tpostpos  6499  snriota  6580  tfrlem11  6649  elixpsn  7101  ixpsnf1o  7102  en1b  7175  mapsnen  7184  xpassen  7202  cantnfp1lem3  7636  wemapwe  7654  oef1o  7655  axdc4lem  8335  ttukeylem3  8391  ttukey2g  8396  fpwwe2lem13  8517  fztp  11102  fzsuc2  11104  fseq1p1m1  11122  fseq1m1p1  11123  expval  11384  s1val  11752  s1eq  11753  fsumm1  12537  divalgmod  12926  vdwpc  13348  vdwlem1  13349  vdwlem6  13354  vdwlem7  13355  vdwlem8  13356  setsvalg  13492  strle1  13560  imasval  13737  imasaddvallem  13754  imasvscaval  13763  ismri2dad  13862  mreexd  13867  mreexmrid  13868  homaval  14186  setcmon  14242  pwsco2mhm  14770  gsumress  14777  mulgval  14892  symgval  15094  gsumzsubmcl  15523  gsumzaddlem  15526  pwsgsum  15553  dmdprd  15559  dprdval  15561  subgdmdprd  15592  dprdsn  15594  dprd2da  15600  dmdprdpr  15607  dprdpr  15608  dpjfval  15613  dpjval  15614  ablfac1eulem  15630  pgpfaclem1  15639  isunit  15762  isdrng  15839  drngprop  15846  isdrngd  15860  drngpropd  15862  issubdrg  15893  lspsnneg  16082  lspsnsub  16083  lmodindp1  16090  islbs  16148  lspsntrim  16170  lbspropd  16171  lspsnvs  16186  lspsneleq  16187  lspfixed  16200  lpival  16316  psrval  16429  mplval  16492  ressmplbas2  16518  mplbaspropd  16630  zrhrhmb  16792  znval  16816  isobs  16947  ordtval  17253  ordtcnv  17265  ptval2  17633  dfac14  17650  txdis  17664  xkoptsub  17686  pt1hmeo  17838  xpstopnlem1  17841  xpstopnlem2  17843  tgptsmscls  18179  ustuqtoplem  18269  utopsnneiplem  18277  utopsnneip  18278  utop2nei  18280  utop3cls  18281  pcorev2  19053  pcophtb  19054  pi1grplem  19074  pi1inv  19077  i1f1  19582  i1faddlem  19585  i1fmullem  19586  i1fadd  19587  limcfval  19759  dvnfval  19808  mdegfval  19985  mdegpropd  20007  ig1pval  20095  0dgrb  20165  dgreq0  20183  dgrmulc  20189  plyrem  20222  facth  20223  fta1  20225  aaliou2  20257  taylpfval  20281  1pthoncl  21592  2pthlem2  21596  eupath2lem3  21701  drngoi  21995  isdivrngo  22019  0ofval  22288  indval2  24412  sitgval  24647  subfacp1lem5  24870  sconpht  24916  sconpht2  24925  sconpi1  24926  cvmliftlem7  24978  cvmliftlem10  24981  cvmlift2lem13  25002  cvmlift3lem9  25014  fprodm1  25290  axlowdimlem15  25895  axlowdim  25900  onint1  26199  grpokerinj  26560  isprrngo  26660  ralxpmap  26742  dfac11  27137  dfac21  27141  frlmval  27193  frlmgsum  27209  uvcresum  27219  frlmlbs  27226  frlmup1  27227  islindf  27259  lindfmm  27274  lsslindf  27277  islindf4  27285  islindf5  27286  dgrnznn  27317  expgrowth  27529  dfateq12d  27969  otsndisj  28065  otiunsndisj  28066  otiunsndisjX  28067  cshwsdisj  28285  frgrancvvdeqlem4  28422  frgrancvvdeqlem6  28424  bnj941  29143  bnj944  29309  lsatset  29788  lsmsat  29806  islshpat  29815  lflsc0N  29881  lkrfval  29885  ldualset  29923  dvafset  31801  dvaset  31802  dvhfset  31878  dvhset  31879  dibffval  31938  dibfval  31939  dib0  31962  cdlemn4a  31997  dihmeetlem4preN  32104  dihmeetlem13N  32117  dih1dimatlem  32127  dihlsprn  32129  dvh2dim  32243  lpolsetN  32280  lclkrlem2j  32314  lclkrlem2p  32320  lcfrlem21  32361  mapdpglem22  32491  mapdpglem23  32492  mapdpglem26  32496  mapdpglem27  32497  mapdpg  32504  baerlem3lem2  32508  baerlem5alem2  32509  baerlem5blem2  32510  baerlem5amN  32514  baerlem5bmN  32515  baerlem5abmN  32516  mapdindp4  32521  mapdhval  32522  mapdheq  32526  mapdh6aN  32533  hvmapffval  32556  hvmapfval  32557  hvmap1o2  32563  hdmap1fval  32595  hdmap1vallem  32596  hdmap1val  32597  hdmap1eq  32600  hdmap1cbv  32601  hdmap1l6a  32608  hdmap1neglem1N  32626  hdmapfval  32628  hdmap10  32641  hdmaprnlem6N  32655  hgmaprnlem2N  32698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-sn 3820
  Copyright terms: Public domain W3C validator