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

Theorem sneqd 4382
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sneqd (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2 (𝜑𝐴 = 𝐵)
2 sneq 4380 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 17 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {csn 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-sn 4371
This theorem is referenced by:  otsndisj  5174  otiunsndisj  5175  iunopeqop  5176  dmsnopss  5819  dmsnsnsn  5825  cnvsngOLD  5835  opswap  5836  ressn  5885  f1osng  6389  fsng  6623  fsn2g  6624  funopsn  6633  funsneqopsnOLD  6637  funsneqopb  6639  fnressn  6645  fvsng  6668  2nd1st  7441  dfmpt2  7497  cnvf1olem  7505  suppsnop  7539  tpostpos  7603  tfrlem11  7716  ralxpmap  8140  elixpsn  8180  ixpsnf1o  8181  en1b  8256  mapsnend  8267  xpassen  8289  cantnfp1lem3  8820  axdc4lem  9558  ttukeylem3  9614  ttukey2g  9619  fpwwe2lem13  9745  fztp  12616  fzsuc2  12617  fseq1p1m1  12633  fseq1m1p1  12634  expval  13081  s1val  13589  s1eq  13591  s3sndisj  13927  s3iunsndisj  13928  fsumm1  14699  fprodm1  14914  divalgmod  15345  vdwpc  15897  vdwlem1  15898  vdwlem6  15903  vdwlem7  15904  vdwlem8  15905  cshwsdisj  16013  setsvalg  16094  setsidvald  16096  strle1  16180  imasval  16372  imasaddvallem  16390  imasvscaval  16399  ismri2dad  16498  mreexd  16503  mreexmrid  16504  homaval  16881  setcmon  16937  funcsetcestrclem1  16995  gsumress  17477  pwsco2mhm  17572  mulgval  17744  symgval  17996  idressubgsymg  18027  gsumzaddlem  18518  dmdprd  18595  subgdmdprd  18631  dprdsn  18633  dprd2da  18639  dmdprdpr  18646  dprdpr  18647  dpjfval  18652  dpjval  18653  ablfac1eulem  18669  pgpfaclem1  18678  isunit  18855  isdrng  18951  drngprop  18958  isdrngd  18972  drngpropd  18974  issubdrg  19005  lspsnneg  19209  lspsnsub  19210  lmodindp1  19217  islbs  19279  lspsntrim  19301  lbspropd  19302  lspsnvs  19317  lspsneleq  19318  lspfixed  19331  lspfixedOLD  19332  lpival  19450  psrval  19567  zrhrhmb  20063  znval  20087  isobs  20270  frlmval  20298  frlmlbs  20342  islindf  20357  lindfmm  20372  lsslindf  20375  islindf4  20383  islindf5  20384  mat1dimmul  20489  mat1dimcrng  20490  mat1rhmval  20492  mat1ric  20500  mat1scmat  20552  mdet0pr  20605  m1detdiag  20610  pmatcoe1fsupp  20715  ordtval  21203  ordtcnv  21215  dissnlocfin  21542  ptval2  21614  dfac14  21631  txdis  21645  xkoptsub  21667  pt1hmeo  21819  xpstopnlem1  21822  xpstopnlem2  21824  tgptsmscls  22162  ustuqtoplem  22252  utopsnneiplem  22260  utopsnneip  22261  utop2nei  22263  utop3cls  22264  pcorev2  23036  pcophtb  23037  pi1grplem  23057  pi1inv  23060  cvsunit  23139  i1f1  23667  i1faddlem  23670  i1fmullem  23671  i1fadd  23672  limcfval  23846  dvnfval  23895  ig1pval  24142  0dgrb  24212  dgrnznn  24213  dgreq0  24231  dgrmulc  24237  plyrem  24270  facth  24271  fta1  24273  aaliou2  24305  taylpfval  24329  axlowdimlem15  26046  axlowdim  26051  1loopgruspgr  26620  1egrvtxdg1r  26630  1egrvtxdg0  26631  wkslem1  26727  wkslem2  26728  iswlk  26730  redwlk  26793  wlkp1lem8  26801  crctcshwlkn0lem4  26930  crctcshwlkn0lem5  26931  crctcshwlkn0lem6  26932  loopclwwlkn1b  27187  clwwlkn1loopb  27188  clwwlknon1  27261  eupth2lem3lem3  27399  frgrncvvdeqlem3  27472  frgrncvvdeqlem5  27474  wlkl0  27543  0ofval  27966  fcnvgreu  29795  dispcmp  30247  ordtprsval  30285  ordtprsuni  30286  indval2  30397  sitgval  30715  sseqval  30771  reprsuc  31014  bnj941  31161  bnj944  31326  subfacp1lem5  31484  sconnpht  31529  sconnpht2  31538  sconnpi1  31539  cvmliftlem7  31591  cvmliftlem10  31594  cvmlift2lem13  31615  cvmlift3lem9  31627  msrval  31753  mthmpps  31797  nosupbnd2lem1  32177  nosupbnd2  32178  onint1  32760  bj-projeq  33285  bj-restsn  33341  finixpnum  33702  matunitlindflem1  33713  ptrest  33716  poimirlem4  33721  poimirlem13  33730  poimirlem14  33731  poimirlem16  33733  poimirlem19  33736  poimirlem26  33743  grpokerinj  33998  isdivrngo  34055  drngoi  34056  isprrngo  34155  lsatset  34765  lsmsat  34783  islshpat  34792  lflsc0N  34858  lkrfval  34862  ldualset  34900  dvafset  36779  dvaset  36780  dvhfset  36855  dvhset  36856  dibffval  36915  dibfval  36916  dib0  36939  cdlemn4a  36974  dihmeetlem4preN  37081  dihmeetlem13N  37094  dih1dimatlem  37104  dihlsprn  37106  dvh2dim  37220  lpolsetN  37257  lclkrlem2j  37291  lclkrlem2p  37297  lcfrlem21  37338  mapdpglem22  37468  mapdpglem23  37469  mapdpglem26  37473  mapdpglem27  37474  mapdpg  37481  baerlem3lem2  37485  baerlem5alem2  37486  baerlem5blem2  37487  baerlem5amN  37491  baerlem5bmN  37492  baerlem5abmN  37493  mapdindp4  37498  mapdhval  37499  mapdheq  37503  mapdh6aN  37510  hvmapffval  37533  hvmapfval  37534  hvmap1o2  37540  hdmap1fval  37571  hdmap1vallem  37572  hdmap1val  37573  hdmap1eq  37576  hdmap1cbv  37577  hdmap1l6a  37584  hdmapfval  37602  hdmap10  37615  hdmaprnlem6N  37629  hgmaprnlem2N  37672  dfac11  38127  dfac21  38131  nzprmdif  39012  expgrowth  39028  fzdifsuc2  39999  cnrefiisplem  40529  cnrefiisp  40530  hoidmv1le  41284  ovnovollem3  41348  dfateq12d  41709  otiunsndisjX  41863  funop1  41867  lmod1zr  42844
  Copyright terms: Public domain W3C validator