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

Theorem sneqd 3787
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 3785 . 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 3774
This theorem is referenced by:  dmsnopss  5301  dmsnsnsn  5307  cnvsng  5314  opswap  5315  ressn  5367  f1osng  5675  fsng  5866  fnressn  5877  fvsng  5886  2nd1st  6351  dfmpt2  6396  cnvf1olem  6403  tpostpos  6458  snriota  6539  tfrlem11  6608  elixpsn  7060  ixpsnf1o  7061  en1b  7134  mapsnen  7143  xpassen  7161  cantnfp1lem3  7592  wemapwe  7610  oef1o  7611  axdc4lem  8291  ttukeylem3  8347  ttukey2g  8352  fpwwe2lem13  8473  fztp  11058  fzsuc2  11060  fseq1p1m1  11077  fseq1m1p1  11078  expval  11339  s1val  11707  s1eq  11708  fsumm1  12492  divalgmod  12881  vdwpc  13303  vdwlem1  13304  vdwlem6  13309  vdwlem7  13310  vdwlem8  13311  setsvalg  13447  strle1  13515  imasval  13692  imasaddvallem  13709  imasvscaval  13718  ismri2dad  13817  mreexd  13822  mreexmrid  13823  homaval  14141  setcmon  14197  pwsco2mhm  14725  gsumress  14732  mulgval  14847  symgval  15049  gsumzsubmcl  15478  gsumzaddlem  15481  pwsgsum  15508  dmdprd  15514  dprdval  15516  subgdmdprd  15547  dprdsn  15549  dprd2da  15555  dmdprdpr  15562  dprdpr  15563  dpjfval  15568  dpjval  15569  ablfac1eulem  15585  pgpfaclem1  15594  isunit  15717  isdrng  15794  drngprop  15801  isdrngd  15815  drngpropd  15817  issubdrg  15848  lspsnneg  16037  lspsnsub  16038  lmodindp1  16045  islbs  16103  lspsntrim  16125  lbspropd  16126  lspsnvs  16141  lspsneleq  16142  lspfixed  16155  lpival  16271  psrval  16384  mplval  16447  ressmplbas2  16473  mplbaspropd  16585  zrhrhmb  16747  znval  16771  isobs  16902  ordtval  17207  ordtcnv  17219  ptval2  17586  dfac14  17603  txdis  17617  xkoptsub  17639  pt1hmeo  17791  xpstopnlem1  17794  xpstopnlem2  17796  tgptsmscls  18132  ustuqtoplem  18222  utopsnneiplem  18230  utopsnneip  18231  utop2nei  18233  utop3cls  18234  pcorev2  19006  pcophtb  19007  pi1grplem  19027  pi1inv  19030  i1f1  19535  i1faddlem  19538  i1fmullem  19539  i1fadd  19540  limcfval  19712  dvnfval  19761  mdegfval  19938  mdegpropd  19960  ig1pval  20048  0dgrb  20118  dgreq0  20136  dgrmulc  20142  plyrem  20175  facth  20176  fta1  20178  aaliou2  20210  taylpfval  20234  1pthoncl  21545  2pthlem2  21549  eupath2lem3  21654  drngoi  21948  isdivrngo  21972  0ofval  22241  indval2  24365  sitgval  24600  subfacp1lem5  24823  sconpht  24869  sconpht2  24878  sconpi1  24879  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem13  24955  cvmlift3lem9  24967  fprodm1  25243  axlowdimlem15  25799  axlowdim  25804  onint1  26103  grpokerinj  26450  isprrngo  26550  ralxpmap  26632  dfac11  27028  dfac21  27032  frlmval  27084  frlmgsum  27100  uvcresum  27110  frlmlbs  27117  frlmup1  27118  islindf  27150  lindfmm  27165  lsslindf  27168  islindf4  27176  islindf5  27177  dgrnznn  27208  expgrowth  27420  dfateq12d  27860  otsndisj  27953  otiunsndisj  27954  otiunsndisjX  27955  frgrancvvdeqlem4  28136  frgrancvvdeqlem6  28138  bnj941  28849  bnj944  29015  lsatset  29473  lsmsat  29491  islshpat  29500  lflsc0N  29566  lkrfval  29570  ldualset  29608  dvafset  31486  dvaset  31487  dvhfset  31563  dvhset  31564  dibffval  31623  dibfval  31624  dib0  31647  cdlemn4a  31682  dihmeetlem4preN  31789  dihmeetlem13N  31802  dih1dimatlem  31812  dihlsprn  31814  dvh2dim  31928  lpolsetN  31965  lclkrlem2j  31999  lclkrlem2p  32005  lcfrlem21  32046  mapdpglem22  32176  mapdpglem23  32177  mapdpglem26  32181  mapdpglem27  32182  mapdpg  32189  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdindp4  32206  mapdhval  32207  mapdheq  32211  mapdh6aN  32218  hvmapffval  32241  hvmapfval  32242  hvmap1o2  32248  hdmap1fval  32280  hdmap1vallem  32281  hdmap1val  32282  hdmap1eq  32285  hdmap1cbv  32286  hdmap1l6a  32293  hdmap1neglem1N  32311  hdmapfval  32313  hdmap10  32326  hdmaprnlem6N  32340  hgmaprnlem2N  32383
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 2385
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 2391  df-cleq 2397  df-sn 3780
  Copyright terms: Public domain W3C validator