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

Theorem sneqd 3653
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 3651 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 15 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {csn 3640
This theorem is referenced by:  dmsnopss  5145  dmsnsnsn  5151  cnvsng  5158  opswap  5159  ressn  5211  f1osng  5514  fsng  5697  fnressn  5705  fvsng  5714  2nd1st  6165  dfmpt2  6209  cnvf1olem  6216  tpostpos  6254  snriota  6335  tfrlem11  6404  elixpsn  6855  ixpsnf1o  6856  en1b  6929  mapsnen  6938  xpassen  6956  cantnfp1lem3  7382  wemapwe  7400  oef1o  7401  axdc4lem  8081  ttukeylem3  8138  ttukey2g  8143  fpwwe2lem13  8264  fztp  10841  fzsuc2  10842  fseq1p1m1  10857  fseq1m1p1  10858  expval  11106  s1val  11438  s1eq  11439  fsumm1  12216  divalgmod  12605  vdwpc  13027  vdwlem1  13028  vdwlem6  13033  vdwlem7  13034  vdwlem8  13035  setsvalg  13171  strle1  13239  imasval  13414  imasaddvallem  13431  imasvscaval  13440  ismri2dad  13539  mreexd  13544  mreexmrid  13545  homaval  13863  setcmon  13919  pwsco2mhm  14447  gsumress  14454  mulgval  14569  symgval  14771  gsumzsubmcl  15200  gsumzaddlem  15203  pwsgsum  15230  dmdprd  15236  dprdval  15238  subgdmdprd  15269  dprdsn  15271  dprd2da  15277  dmdprdpr  15284  dprdpr  15285  dpjfval  15290  dpjval  15291  ablfac1eulem  15307  pgpfaclem1  15316  isunit  15439  isdrng  15516  drngprop  15523  isdrngd  15537  drngpropd  15539  issubdrg  15570  lspsnneg  15763  lspsnsub  15764  lmodindp1  15771  islbs  15829  lspsntrim  15851  lbspropd  15852  lspsnvs  15867  lspsneleq  15868  lspfixed  15881  lpival  15997  psrval  16110  mplval  16173  ressmplbas2  16199  mplbaspropd  16314  zrhrhmb  16465  znval  16489  isobs  16620  ordtval  16919  ordtcnv  16931  ptval2  17296  dfac14  17312  txdis  17326  xkoptsub  17348  pt1hmeo  17497  xpstopnlem1  17500  xpstopnlem2  17502  tgptsmscls  17832  pcorev2  18526  pcophtb  18527  pi1grplem  18547  pi1inv  18550  i1f1  19045  i1faddlem  19048  i1fmullem  19049  i1fadd  19050  limcfval  19222  dvnfval  19271  mdegfval  19448  mdegpropd  19470  ig1pval  19558  0dgrb  19628  dgreq0  19646  dgrmulc  19652  plyrem  19685  facth  19686  fta1  19688  aaliou2  19720  taylpfval  19744  drngoi  21074  isdivrngo  21098  0ofval  21365  indval2  23598  subfacp1lem5  23715  sconpht  23760  sconpht2  23769  sconpi1  23770  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift2lem13  23846  cvmlift3lem9  23858  eupath2lem3  23903  axlowdimlem15  24584  axlowdim  24589  onint1  24888  imfstnrelc  25081  cbicp  25166  cndpv  26049  pgapspf  26052  grpokerinj  26575  isprrngo  26675  ralxpmap  26761  dfac11  27160  dfac21  27164  frlmval  27216  frlmgsum  27232  uvcresum  27242  frlmlbs  27249  frlmup1  27250  islindf  27282  lindfmm  27297  lsslindf  27300  islindf4  27308  islindf5  27309  dgrnznn  27340  expgrowth  27552  dfateq12d  27992  bnj941  28804  bnj944  28970  lsatset  29180  lsmsat  29198  islshpat  29207  lflsc0N  29273  lkrfval  29277  ldualset  29315  dvafset  31193  dvaset  31194  dvhfset  31270  dvhset  31271  dibffval  31330  dibfval  31331  dib0  31354  cdlemn4a  31389  dihmeetlem4preN  31496  dihmeetlem13N  31509  dih1dimatlem  31519  dihlsprn  31521  dvh2dim  31635  lpolsetN  31672  lclkrlem2j  31706  lclkrlem2p  31712  lcfrlem21  31753  mapdpglem22  31883  mapdpglem23  31884  mapdpglem26  31888  mapdpglem27  31889  mapdpg  31896  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdindp4  31913  mapdhval  31914  mapdheq  31918  mapdh6aN  31925  hvmapffval  31948  hvmapfval  31949  hvmap1o2  31955  hdmap1fval  31987  hdmap1vallem  31988  hdmap1val  31989  hdmap1eq  31992  hdmap1cbv  31993  hdmap1l6a  32000  hdmap1neglem1N  32018  hdmapfval  32020  hdmap10  32033  hdmaprnlem6N  32047  hgmaprnlem2N  32090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-sn 3646
  Copyright terms: Public domain W3C validator