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

Theorem sneqd 3986
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 3984 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 17 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407   {csn 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-sn 3975
This theorem is referenced by:  otsndisj  4697  otiunsndisj  4698  dmsnopss  5298  dmsnsnsn  5304  cnvsng  5312  opswap  5313  ressn  5362  f1osng  5839  fsng  6052  fsn2g  6053  fnressn  6065  fvsng  6087  2nd1st  6831  dfmpt2  6876  cnvf1olem  6884  suppsnop  6918  tpostpos  6980  tfrlem11  7093  ralxpmap  7508  elixpsn  7548  ixpsnf1o  7549  en1b  7623  mapsnen  7633  xpassen  7651  cantnfp1lem3  8133  cantnfp1lem3OLD  8159  wemapweOLD  8174  oef1oOLD  8176  axdc4lem  8869  ttukeylem3  8925  ttukey2g  8930  fpwwe2lem13  9052  fztp  11793  fzsuc2  11794  fseq1p1m1  11809  fseq1m1p1  11810  expval  12214  s1val  12666  s1eq  12668  fsumm1  13719  fprodm1  13925  divalgmod  14275  vdwpc  14709  vdwlem1  14710  vdwlem6  14715  vdwlem7  14716  vdwlem8  14717  cshwsdisj  14794  setsvalg  14867  setsidvald  14869  strle1  14942  imasval  15127  imasaddvallem  15145  imasvscaval  15154  ismri2dad  15253  mreexd  15258  mreexmrid  15259  homaval  15636  setcmon  15692  funcsetcestrclem1  15749  gsumress  16229  pwsco2mhm  16328  mulgval  16470  symgval  16730  idressubgsymg  16761  gsumzsubmclOLD  17255  gsumzaddlem  17260  gsumzaddlemOLD  17262  pwsgsumOLD  17332  dmdprd  17351  dprdvalOLD  17358  subgdmdprd  17403  dprdsn  17405  dprd2da  17413  dmdprdpr  17420  dprdpr  17421  dpjfval  17426  dpjval  17427  ablfac1eulem  17445  pgpfaclem1  17454  isunit  17628  isdrng  17722  drngprop  17729  isdrngd  17743  drngpropd  17745  issubdrg  17776  lspsnneg  17974  lspsnsub  17975  lmodindp1  17982  islbs  18044  lspsntrim  18066  lbspropd  18067  lspsnvs  18082  lspsneleq  18083  lspfixed  18096  lpival  18215  psrval  18333  zrhrhmb  18850  znval  18874  isobs  19051  frlmval  19079  frlmgsumOLD  19099  frlmlbs  19126  islindf  19141  lindfmm  19156  lsslindf  19159  islindf4  19167  islindf5  19168  mat1dimmul  19272  mat1dimcrng  19273  mat1rhmval  19275  mat1ric  19283  mat1scmat  19335  mdet0pr  19388  m1detdiag  19393  pmatcoe1fsupp  19496  ordtval  19985  ordtcnv  19997  dissnlocfin  20324  ptval2  20396  dfac14  20413  txdis  20427  xkoptsub  20449  pt1hmeo  20601  xpstopnlem1  20604  xpstopnlem2  20606  tgptsmscls  20946  ustuqtoplem  21036  utopsnneiplem  21044  utopsnneip  21045  utop2nei  21047  utop3cls  21048  pcorev2  21822  pcophtb  21823  pi1grplem  21843  pi1inv  21846  cvsunit  21902  i1f1  22391  i1faddlem  22394  i1fmullem  22395  i1fadd  22396  limcfval  22570  dvnfval  22619  ig1pval  22867  0dgrb  22937  dgrnznn  22938  dgreq0  22956  dgrmulc  22962  plyrem  22995  facth  22996  fta1  22998  aaliou2  23030  taylpfval  23054  axlowdimlem15  24688  axlowdim  24693  1pthoncl  25023  2pthlem2  25027  eupath2lem3  25408  frgrancvvdeqlem4  25462  frgrancvvdeqlem6  25464  drngoi  25836  isdivrngo  25860  0ofval  26129  fcnvgreu  27970  dispcmp  28328  ordtprsval  28366  ordtprsuni  28367  indval2  28475  sitgval  28793  sseqval  28846  bnj941  29171  bnj944  29336  subfacp1lem5  29494  sconpht  29539  sconpht2  29548  sconpi1  29549  cvmliftlem7  29601  cvmliftlem10  29604  cvmlift2lem13  29625  cvmlift3lem9  29637  msrval  29763  mthmpps  29807  onint1  30694  bj-projeq  31128  finixpnum  31423  ptrest  31433  grpokerinj  31642  isprrngo  31742  lsatset  32021  lsmsat  32039  islshpat  32048  lflsc0N  32114  lkrfval  32118  ldualset  32156  dvafset  34036  dvaset  34037  dvhfset  34113  dvhset  34114  dibffval  34173  dibfval  34174  dib0  34197  cdlemn4a  34232  dihmeetlem4preN  34339  dihmeetlem13N  34352  dih1dimatlem  34362  dihlsprn  34364  dvh2dim  34478  lpolsetN  34515  lclkrlem2j  34549  lclkrlem2p  34555  lcfrlem21  34596  mapdpglem22  34726  mapdpglem23  34727  mapdpglem26  34731  mapdpglem27  34732  mapdpg  34739  baerlem3lem2  34743  baerlem5alem2  34744  baerlem5blem2  34745  baerlem5amN  34749  baerlem5bmN  34750  baerlem5abmN  34751  mapdindp4  34756  mapdhval  34757  mapdheq  34761  mapdh6aN  34768  hvmapffval  34791  hvmapfval  34792  hvmap1o2  34798  hdmap1fval  34830  hdmap1vallem  34831  hdmap1val  34832  hdmap1eq  34835  hdmap1cbv  34836  hdmap1l6a  34843  hdmap1neglem1N  34861  hdmapfval  34863  hdmap10  34876  hdmaprnlem6N  34890  hgmaprnlem2N  34933  dfac11  35383  dfac21  35387  nzprmdif  36085  expgrowth  36101  fzdifsuc2  36894  dfateq12d  37595  otiunsndisjX  37947  lmod1zr  38618
  Copyright terms: Public domain W3C validator