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

Theorem sneqd 3980
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 3978 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 17 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444   {csn 3968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-sn 3969
This theorem is referenced by:  otsndisj  4706  otiunsndisj  4707  dmsnopss  5308  dmsnsnsn  5314  cnvsng  5322  opswap  5323  ressn  5372  f1osng  5853  fsng  6063  fsn2g  6064  fnressn  6076  fvsng  6098  2nd1st  6838  dfmpt2  6886  cnvf1olem  6894  suppsnop  6928  tpostpos  6993  tfrlem11  7106  ralxpmap  7521  elixpsn  7561  ixpsnf1o  7562  en1b  7637  mapsnen  7647  xpassen  7666  cantnfp1lem3  8185  axdc4lem  8885  ttukeylem3  8941  ttukey2g  8946  fpwwe2lem13  9067  fztp  11852  fzsuc2  11853  fseq1p1m1  11868  fseq1m1p1  11869  expval  12274  s1val  12737  s1eq  12739  fsumm1  13812  fprodm1  14021  divalgmod  14387  vdwpc  14930  vdwlem1  14931  vdwlem6  14936  vdwlem7  14937  vdwlem8  14938  cshwsdisj  15069  setsvalg  15145  setsidvald  15147  strle1  15221  imasval  15411  imasvalOLD  15412  imasaddvallem  15435  imasvscaval  15444  ismri2dad  15543  mreexd  15548  mreexmrid  15549  homaval  15926  setcmon  15982  funcsetcestrclem1  16039  gsumress  16519  pwsco2mhm  16618  mulgval  16760  symgval  17020  idressubgsymg  17051  gsumzaddlem  17554  dmdprd  17630  subgdmdprd  17667  dprdsn  17669  dprd2da  17675  dmdprdpr  17682  dprdpr  17683  dpjfval  17688  dpjval  17689  ablfac1eulem  17705  pgpfaclem1  17714  isunit  17885  isdrng  17979  drngprop  17986  isdrngd  18000  drngpropd  18002  issubdrg  18033  lspsnneg  18229  lspsnsub  18230  lmodindp1  18237  islbs  18299  lspsntrim  18321  lbspropd  18322  lspsnvs  18337  lspsneleq  18338  lspfixed  18351  lpival  18469  psrval  18586  zrhrhmb  19082  znval  19106  isobs  19283  frlmval  19311  frlmlbs  19355  islindf  19370  lindfmm  19385  lsslindf  19388  islindf4  19396  islindf5  19397  mat1dimmul  19501  mat1dimcrng  19502  mat1rhmval  19504  mat1ric  19512  mat1scmat  19564  mdet0pr  19617  m1detdiag  19622  pmatcoe1fsupp  19725  ordtval  20205  ordtcnv  20217  dissnlocfin  20544  ptval2  20616  dfac14  20633  txdis  20647  xkoptsub  20669  pt1hmeo  20821  xpstopnlem1  20824  xpstopnlem2  20826  tgptsmscls  21164  ustuqtoplem  21254  utopsnneiplem  21262  utopsnneip  21263  utop2nei  21265  utop3cls  21266  pcorev2  22059  pcophtb  22060  pi1grplem  22080  pi1inv  22083  cvsunit  22139  i1f1  22648  i1faddlem  22651  i1fmullem  22652  i1fadd  22653  limcfval  22827  dvnfval  22876  ig1pval  23124  ig1pvalOLD  23130  0dgrb  23200  dgrnznn  23201  dgreq0  23219  dgrmulc  23225  plyrem  23258  facth  23259  fta1  23261  aaliou2  23296  taylpfval  23320  axlowdimlem15  24986  axlowdim  24991  1pthoncl  25322  2pthlem2  25326  eupath2lem3  25707  frgrancvvdeqlem4  25761  frgrancvvdeqlem6  25763  drngoi  26135  isdivrngo  26159  0ofval  26428  fcnvgreu  28275  dispcmp  28686  ordtprsval  28724  ordtprsuni  28725  indval2  28836  sitgval  29165  sseqval  29221  bnj941  29584  bnj944  29749  subfacp1lem5  29907  sconpht  29952  sconpht2  29961  sconpi1  29962  cvmliftlem7  30014  cvmliftlem10  30017  cvmlift2lem13  30038  cvmlift3lem9  30050  msrval  30176  mthmpps  30220  onint1  31109  bj-projeq  31586  finixpnum  31930  ptrest  31939  poimirlem4  31944  poimirlem13  31953  poimirlem14  31954  poimirlem16  31956  poimirlem19  31959  poimirlem26  31966  grpokerinj  32183  isprrngo  32283  lsatset  32556  lsmsat  32574  islshpat  32583  lflsc0N  32649  lkrfval  32653  ldualset  32691  dvafset  34571  dvaset  34572  dvhfset  34648  dvhset  34649  dibffval  34708  dibfval  34709  dib0  34732  cdlemn4a  34767  dihmeetlem4preN  34874  dihmeetlem13N  34887  dih1dimatlem  34897  dihlsprn  34899  dvh2dim  35013  lpolsetN  35050  lclkrlem2j  35084  lclkrlem2p  35090  lcfrlem21  35131  mapdpglem22  35261  mapdpglem23  35262  mapdpglem26  35266  mapdpglem27  35267  mapdpg  35274  baerlem3lem2  35278  baerlem5alem2  35279  baerlem5blem2  35280  baerlem5amN  35284  baerlem5bmN  35285  baerlem5abmN  35286  mapdindp4  35291  mapdhval  35292  mapdheq  35296  mapdh6aN  35303  hvmapffval  35326  hvmapfval  35327  hvmap1o2  35333  hdmap1fval  35365  hdmap1vallem  35366  hdmap1val  35367  hdmap1eq  35370  hdmap1cbv  35371  hdmap1l6a  35378  hdmap1neglem1N  35396  hdmapfval  35398  hdmap10  35411  hdmaprnlem6N  35425  hgmaprnlem2N  35468  dfac11  35920  dfac21  35924  nzprmdif  36668  expgrowth  36684  mapsnend  37480  fzdifsuc2  37530  hoidmv1le  38416  dfateq12d  38631  iunopeqop  39005  otiunsndisjX  39006  funopsn  39018  funop1  39020  funsneqopsn  39023  is1wlk  39628  1wlk1walk  39648  lmod1zr  40339
  Copyright terms: Public domain W3C validator