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

Theorem sneqd 3910
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 3908 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   {csn 3898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-sn 3899
This theorem is referenced by:  dmsnopss  5332  dmsnsnsn  5338  cnvsng  5346  opswap  5347  ressn  5394  f1osng  5700  fsng  5903  fnressn  5915  fvsng  5933  2nd1st  6640  dfmpt2  6684  cnvf1olem  6691  suppsnop  6725  tpostpos  6786  tfrlem11  6868  ralxpmap  7283  elixpsn  7323  ixpsnf1o  7324  en1b  7398  mapsnen  7408  xpassen  7426  cantnfp1lem3  7909  cantnfp1lem3OLD  7935  wemapweOLD  7950  oef1oOLD  7952  axdc4lem  8645  ttukeylem3  8701  ttukey2g  8706  fpwwe2lem13  8830  fztp  11533  fzsuc2  11535  fseq1p1m1  11555  fseq1m1p1  11556  expval  11888  s1val  12311  s1eq  12312  fsumm1  13241  divalgmod  13631  vdwpc  14062  vdwlem1  14063  vdwlem6  14068  vdwlem7  14069  vdwlem8  14070  cshwsdisj  14146  setsvalg  14218  strle1  14290  imasval  14470  imasaddvallem  14488  imasvscaval  14497  ismri2dad  14596  mreexd  14601  mreexmrid  14602  homaval  14920  setcmon  14976  pwsco2mhm  15520  gsumress  15528  mulgval  15650  symgval  15905  idressubgsymg  15936  gsumzsubmclOLD  16424  gsumzaddlem  16429  gsumzaddlemOLD  16431  pwsgsumOLD  16496  dmdprd  16502  dprdvalOLD  16509  subgdmdprd  16553  dprdsn  16555  dprd2da  16563  dmdprdpr  16570  dprdpr  16571  dpjfval  16576  dpjval  16577  ablfac1eulem  16595  pgpfaclem1  16604  isunit  16771  isdrng  16858  drngprop  16865  isdrngd  16879  drngpropd  16881  issubdrg  16912  lspsnneg  17109  lspsnsub  17110  lmodindp1  17117  islbs  17179  lspsntrim  17201  lbspropd  17202  lspsnvs  17217  lspsneleq  17218  lspfixed  17231  lpival  17349  psrval  17451  zrhrhmb  17964  znval  17988  isobs  18167  frlmval  18195  frlmgsumOLD  18217  frlmlbs  18247  islindf  18263  lindfmm  18278  lsslindf  18281  islindf4  18289  islindf5  18290  mdet0pr  18425  ordtval  18815  ordtcnv  18827  ptval2  19196  dfac14  19213  txdis  19227  xkoptsub  19249  pt1hmeo  19401  xpstopnlem1  19404  xpstopnlem2  19406  tgptsmscls  19746  ustuqtoplem  19836  utopsnneiplem  19844  utopsnneip  19845  utop2nei  19847  utop3cls  19848  pcorev2  20622  pcophtb  20623  pi1grplem  20643  pi1inv  20646  cvsunit  20702  i1f1  21190  i1faddlem  21193  i1fmullem  21194  i1fadd  21195  limcfval  21369  dvnfval  21418  ig1pval  21666  0dgrb  21736  dgreq0  21754  dgrmulc  21760  plyrem  21793  facth  21794  fta1  21796  aaliou2  21828  taylpfval  21852  axlowdimlem15  23224  axlowdim  23229  1pthoncl  23513  2pthlem2  23517  eupath2lem3  23622  drngoi  23916  isdivrngo  23940  0ofval  24209  fcnvgreu  26013  ordtprsval  26370  ordtprsuni  26371  ordtcnvNEW  26372  indval2  26493  sitgval  26740  sseqval  26793  subfacp1lem5  27094  sconpht  27140  sconpht2  27149  sconpi1  27150  cvmliftlem7  27202  cvmliftlem10  27205  cvmlift2lem13  27226  cvmlift3lem9  27238  fprodm1  27499  onint1  28317  finixpnum  28440  ptrest  28451  grpokerinj  28776  isprrngo  28876  dfac11  29441  dfac21  29445  dgrnznn  29518  expgrowth  29635  dfateq12d  30061  otsndisj  30157  otiunsndisj  30158  otiunsndisjX  30159  frgrancvvdeqlem4  30652  frgrancvvdeqlem6  30654  mat1dimmul  30911  mat1dimcrng  30912  m1detdiag  30931  lmod1zr  31032  pmatcoe1fsupp  31107  bnj941  31862  bnj944  32027  bj-projeq  32581  lsatset  32731  lsmsat  32749  islshpat  32758  lflsc0N  32824  lkrfval  32828  ldualset  32866  dvafset  34744  dvaset  34745  dvhfset  34821  dvhset  34822  dibffval  34881  dibfval  34882  dib0  34905  cdlemn4a  34940  dihmeetlem4preN  35047  dihmeetlem13N  35060  dih1dimatlem  35070  dihlsprn  35072  dvh2dim  35186  lpolsetN  35223  lclkrlem2j  35257  lclkrlem2p  35263  lcfrlem21  35304  mapdpglem22  35434  mapdpglem23  35435  mapdpglem26  35439  mapdpglem27  35440  mapdpg  35447  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  baerlem5amN  35457  baerlem5bmN  35458  baerlem5abmN  35459  mapdindp4  35464  mapdhval  35465  mapdheq  35469  mapdh6aN  35476  hvmapffval  35499  hvmapfval  35500  hvmap1o2  35506  hdmap1fval  35538  hdmap1vallem  35539  hdmap1val  35540  hdmap1eq  35543  hdmap1cbv  35544  hdmap1l6a  35551  hdmap1neglem1N  35569  hdmapfval  35571  hdmap10  35584  hdmaprnlem6N  35598  hgmaprnlem2N  35641
  Copyright terms: Public domain W3C validator