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

Theorem sneqd 4160
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 4158 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 17 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {csn 4148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-sn 4149
This theorem is referenced by:  otsndisj  4939  otiunsndisj  4940  iunopeqop  4941  dmsnopss  5566  dmsnsnsn  5572  cnvsng  5580  opswap  5581  ressn  5630  f1osng  6134  fsng  6358  fsn2g  6359  funopsn  6367  funsneqopsn  6371  fnressn  6379  fvsng  6401  2nd1st  7158  dfmpt2  7212  cnvf1olem  7220  suppsnop  7254  tpostpos  7317  tfrlem11  7429  ralxpmap  7851  elixpsn  7891  ixpsnf1o  7892  en1b  7968  mapsnen  7979  xpassen  7998  cantnfp1lem3  8521  axdc4lem  9221  ttukeylem3  9277  ttukey2g  9282  fpwwe2lem13  9408  fztp  12339  fzsuc2  12340  fseq1p1m1  12355  fseq1m1p1  12356  expval  12802  s1val  13317  s1eq  13319  s3sndisj  13640  s3iunsndisj  13641  fsumm1  14410  fprodm1  14622  divalgmod  15053  divalgmodOLD  15054  vdwpc  15608  vdwlem1  15609  vdwlem6  15614  vdwlem7  15615  vdwlem8  15616  cshwsdisj  15729  setsvalg  15808  setsidvald  15810  strle1  15894  imasval  16092  imasaddvallem  16110  imasvscaval  16119  ismri2dad  16218  mreexd  16223  mreexmrid  16224  homaval  16602  setcmon  16658  funcsetcestrclem1  16715  gsumress  17197  pwsco2mhm  17292  mulgval  17464  symgval  17720  idressubgsymg  17751  gsumzaddlem  18242  dmdprd  18318  subgdmdprd  18354  dprdsn  18356  dprd2da  18362  dmdprdpr  18369  dprdpr  18370  dpjfval  18375  dpjval  18376  ablfac1eulem  18392  pgpfaclem1  18401  isunit  18578  isdrng  18672  drngprop  18679  isdrngd  18693  drngpropd  18695  issubdrg  18726  lspsnneg  18925  lspsnsub  18926  lmodindp1  18933  islbs  18995  lspsntrim  19017  lbspropd  19018  lspsnvs  19033  lspsneleq  19034  lspfixed  19047  lpival  19164  psrval  19281  zrhrhmb  19778  znval  19802  isobs  19983  frlmval  20011  frlmlbs  20055  islindf  20070  lindfmm  20085  lsslindf  20088  islindf4  20096  islindf5  20097  mat1dimmul  20201  mat1dimcrng  20202  mat1rhmval  20204  mat1ric  20212  mat1scmat  20264  mdet0pr  20317  m1detdiag  20322  pmatcoe1fsupp  20425  ordtval  20903  ordtcnv  20915  dissnlocfin  21242  ptval2  21314  dfac14  21331  txdis  21345  xkoptsub  21367  pt1hmeo  21519  xpstopnlem1  21522  xpstopnlem2  21524  tgptsmscls  21863  ustuqtoplem  21953  utopsnneiplem  21961  utopsnneip  21962  utop2nei  21964  utop3cls  21965  pcorev2  22736  pcophtb  22737  pi1grplem  22757  pi1inv  22760  cvsunit  22839  i1f1  23363  i1faddlem  23366  i1fmullem  23367  i1fadd  23368  limcfval  23542  dvnfval  23591  ig1pval  23836  0dgrb  23906  dgrnznn  23907  dgreq0  23925  dgrmulc  23931  plyrem  23964  facth  23965  fta1  23967  aaliou2  23999  taylpfval  24023  axlowdimlem15  25736  axlowdim  25741  1loopgruspgr  26282  1egrvtxdg1r  26292  1egrvtxdg0  26293  wkslem1  26373  wkslem2  26374  iswlk  26376  redwlk  26438  wlkp1lem8  26446  crctcshwlkn0lem4  26574  crctcshwlkn0lem5  26575  crctcshwlkn0lem6  26576  eupth2lem3lem3  26956  frgrncvvdeqlem4  27030  frgrncvvdeqlem6  27032  0ofval  27491  fcnvgreu  29315  dispcmp  29708  ordtprsval  29746  ordtprsuni  29747  indval2  29858  sitgval  30175  sseqval  30231  bnj941  30551  bnj944  30716  subfacp1lem5  30874  sconnpht  30919  sconnpht2  30928  sconnpi1  30929  cvmliftlem7  30981  cvmliftlem10  30984  cvmlift2lem13  31005  cvmlift3lem9  31017  msrval  31143  mthmpps  31187  noextendltgt  31574  onint1  32090  bj-projeq  32627  bj-restsn  32672  finixpnum  33026  matunitlindflem1  33037  ptrest  33040  poimirlem4  33045  poimirlem13  33054  poimirlem14  33055  poimirlem16  33057  poimirlem19  33060  poimirlem26  33067  grpokerinj  33324  isdivrngo  33381  drngoi  33382  isprrngo  33481  lsatset  33757  lsmsat  33775  islshpat  33784  lflsc0N  33850  lkrfval  33854  ldualset  33892  dvafset  35772  dvaset  35773  dvhfset  35849  dvhset  35850  dibffval  35909  dibfval  35910  dib0  35933  cdlemn4a  35968  dihmeetlem4preN  36075  dihmeetlem13N  36088  dih1dimatlem  36098  dihlsprn  36100  dvh2dim  36214  lpolsetN  36251  lclkrlem2j  36285  lclkrlem2p  36291  lcfrlem21  36332  mapdpglem22  36462  mapdpglem23  36463  mapdpglem26  36467  mapdpglem27  36468  mapdpg  36475  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  baerlem5amN  36485  baerlem5bmN  36486  baerlem5abmN  36487  mapdindp4  36492  mapdhval  36493  mapdheq  36497  mapdh6aN  36504  hvmapffval  36527  hvmapfval  36528  hvmap1o2  36534  hdmap1fval  36566  hdmap1vallem  36567  hdmap1val  36568  hdmap1eq  36571  hdmap1cbv  36572  hdmap1l6a  36579  hdmap1neglem1N  36597  hdmapfval  36599  hdmap10  36612  hdmaprnlem6N  36626  hgmaprnlem2N  36669  dfac11  37112  dfac21  37116  nzprmdif  38000  expgrowth  38016  mapsnend  38865  fzdifsuc2  38989  hoidmv1le  40115  ovnovollem3  40179  dfateq12d  40513  otiunsndisjX  40595  funop1  40599  lmod1zr  41570
  Copyright terms: Public domain W3C validator