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

Theorem sneqd 4039
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 4037 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sn 4028
This theorem is referenced by:  otsndisj  4752  otiunsndisj  4753  dmsnopss  5480  dmsnsnsn  5486  cnvsng  5494  opswap  5495  ressn  5543  f1osng  5854  fsng  6060  fnressn  6073  fvsng  6095  2nd1st  6829  dfmpt2  6873  cnvf1olem  6881  suppsnop  6915  tpostpos  6975  tfrlem11  7057  ralxpmap  7468  elixpsn  7508  ixpsnf1o  7509  en1b  7583  mapsnen  7593  xpassen  7611  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  wemapweOLD  8140  oef1oOLD  8142  axdc4lem  8835  ttukeylem3  8891  ttukey2g  8896  fpwwe2lem13  9020  fztp  11736  fzsuc2  11737  fseq1p1m1  11752  fseq1m1p1  11753  expval  12136  s1val  12574  s1eq  12575  fsumm1  13529  divalgmod  13923  vdwpc  14357  vdwlem1  14358  vdwlem6  14363  vdwlem7  14364  vdwlem8  14365  cshwsdisj  14441  setsvalg  14513  strle1  14586  imasval  14766  imasaddvallem  14784  imasvscaval  14793  ismri2dad  14892  mreexd  14897  mreexmrid  14898  homaval  15216  setcmon  15272  pwsco2mhm  15821  gsumress  15829  mulgval  15954  symgval  16209  idressubgsymg  16240  gsumzsubmclOLD  16732  gsumzaddlem  16737  gsumzaddlemOLD  16739  pwsgsumOLD  16813  dmdprd  16832  dprdvalOLD  16839  subgdmdprd  16883  dprdsn  16885  dprd2da  16893  dmdprdpr  16900  dprdpr  16901  dpjfval  16906  dpjval  16907  ablfac1eulem  16925  pgpfaclem1  16934  isunit  17107  isdrng  17200  drngprop  17207  isdrngd  17221  drngpropd  17223  issubdrg  17254  lspsnneg  17452  lspsnsub  17453  lmodindp1  17460  islbs  17522  lspsntrim  17544  lbspropd  17545  lspsnvs  17560  lspsneleq  17561  lspfixed  17574  lpival  17692  psrval  17810  zrhrhmb  18343  znval  18367  isobs  18546  frlmval  18574  frlmgsumOLD  18596  frlmlbs  18626  islindf  18642  lindfmm  18657  lsslindf  18660  islindf4  18668  islindf5  18669  mat1dimmul  18773  mat1dimcrng  18774  mat1rhmval  18776  mat1ric  18784  mat1scmat  18836  mdet0pr  18889  m1detdiag  18894  pmatcoe1fsupp  18997  ordtval  19484  ordtcnv  19496  ptval2  19865  dfac14  19882  txdis  19896  xkoptsub  19918  pt1hmeo  20070  xpstopnlem1  20073  xpstopnlem2  20075  tgptsmscls  20415  ustuqtoplem  20505  utopsnneiplem  20513  utopsnneip  20514  utop2nei  20516  utop3cls  20517  pcorev2  21291  pcophtb  21292  pi1grplem  21312  pi1inv  21315  cvsunit  21371  i1f1  21860  i1faddlem  21863  i1fmullem  21864  i1fadd  21865  limcfval  22039  dvnfval  22088  ig1pval  22336  0dgrb  22406  dgreq0  22424  dgrmulc  22430  plyrem  22463  facth  22464  fta1  22466  aaliou2  22498  taylpfval  22522  axlowdimlem15  23963  axlowdim  23968  1pthoncl  24298  2pthlem2  24302  eupath2lem3  24683  frgrancvvdeqlem4  24738  frgrancvvdeqlem6  24740  drngoi  25113  isdivrngo  25137  0ofval  25406  fcnvgreu  27214  ordtprsval  27564  ordtprsuni  27565  ordtcnvNEW  27566  indval2  27696  sitgval  27942  sseqval  27995  subfacp1lem5  28296  sconpht  28342  sconpht2  28351  sconpi1  28352  cvmliftlem7  28404  cvmliftlem10  28407  cvmlift2lem13  28428  cvmlift3lem9  28440  fprodm1  28701  onint1  29519  finixpnum  29643  ptrest  29653  grpokerinj  29978  isprrngo  30078  dfac11  30640  dfac21  30644  dgrnznn  30717  nzprmdif  30852  expgrowth  30868  dfateq12d  31709  otiunsndisjX  31796  lmod1zr  32193  bnj941  32928  bnj944  33093  bj-projeq  33649  lsatset  33805  lsmsat  33823  islshpat  33832  lflsc0N  33898  lkrfval  33902  ldualset  33940  dvafset  35818  dvaset  35819  dvhfset  35895  dvhset  35896  dibffval  35955  dibfval  35956  dib0  35979  cdlemn4a  36014  dihmeetlem4preN  36121  dihmeetlem13N  36134  dih1dimatlem  36144  dihlsprn  36146  dvh2dim  36260  lpolsetN  36297  lclkrlem2j  36331  lclkrlem2p  36337  lcfrlem21  36378  mapdpglem22  36508  mapdpglem23  36509  mapdpglem26  36513  mapdpglem27  36514  mapdpg  36521  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527  baerlem5amN  36531  baerlem5bmN  36532  baerlem5abmN  36533  mapdindp4  36538  mapdhval  36539  mapdheq  36543  mapdh6aN  36550  hvmapffval  36573  hvmapfval  36574  hvmap1o2  36580  hdmap1fval  36612  hdmap1vallem  36613  hdmap1val  36614  hdmap1eq  36617  hdmap1cbv  36618  hdmap1l6a  36625  hdmap1neglem1N  36643  hdmapfval  36645  hdmap10  36658  hdmaprnlem6N  36672  hgmaprnlem2N  36715
  Copyright terms: Public domain W3C validator