Theorem sneqd 4601

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 4599	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1540  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4590

This theorem is referenced by:  eqsnuniex  5316  otsndisj  5479  otiunsndisj  5480  iunopeqop  5481  dmsnopss  6187  dmsnsnsn  6193  opswap  6202  ressn  6258  suceqd  6399  f1osng  6841  fsng  7109  fsn2g  7110  funopsn  7120  funsneqopb  7124  fnressn  7130  2nd1st  8017  dfmpo  8081  cnvf1olem  8089  xpord2pred  8124  xpord3pred  8131  suppsnop  8157  tpostpos  8225  tfrlem11  8356  naddcllem  8640  ralxpmap  8869  elixpsn  8910  ixpsnf1o  8911  en1b  8996  mapsnend  9007  xpassen  9035  dif1en  9124  dif1enOLD  9126  en1eqsn  9219  cantnfp1lem3  9633  axdc4lem  10408  ttukeylem3  10464  ttukey2g  10469  fpwwe2lem12  10595  fztp  13541  fzsuc2  13543  fseq1p1m1  13559  fseq1m1p1  13560  expval  14028  hash1elsn  14336  s1val  14563  s1eq  14565  s3sndisj  14933  s3iunsndisj  14934  fsumm1  15717  fprodm1  15933  divalgmod  16376  vdwpc  16951  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  cshwsdisj  17069  strle1  17128  setsvalg  17136  setsidvald  17169  imasval  17474  imasaddvallem  17492  imasvscaval  17501  ismri2dad  17598  mreexd  17603  mreexmrid  17604  homaval  17993  setcmon  18049  funcsetcestrclem1  18115  gsumress  18609  pwsco2mhm  18760  efmnd  18797  idressubmefmnd  18825  smndex1igid  18831  smndex1basss  18832  smndex1mgm  18834  smndex1mndlem  18836  mulgval  19003  idressubgsymg  19340  gsumzaddlem  19851  dmdprd  19930  subgdmdprd  19966  dprdsn  19968  dprd2da  19974  dmdprdpr  19981  dprdpr  19982  dpjfval  19987  dpjval  19988  ablfac1eulem  20004  pgpfaclem1  20013  isunit  20282  isdrng  20642  drngprop  20653  isdrngd  20674  isdrngdOLD  20676  drngpropd  20678  issubdrg  20689  subdrgint  20712  lspsnneg  20912  lspsnsub  20913  lmodindp1  20920  islbs  20983  lspsntrim  21005  lbspropd  21006  lspsnvs  21024  lspsneleq  21025  lspfixed  21038  rngqiprngimf1  21210  lpival  21234  pzriprnglem13  21403  pzriprnglem14  21404  zrhrhmb  21420  znval  21445  isobs  21629  frlmval  21657  frlmlbs  21706  islindf  21721  lindfmm  21736  lsslindf  21739  islindf4  21747  islindf5  21748  psrval  21824  mat1dimmul  22363  mat1dimcrng  22364  mat1rhmval  22366  mat1ric  22374  mat1scmat  22426  mdet0pr  22479  m1detdiag  22484  pmatcoe1fsupp  22588  ordtval  23076  ordtcnv  23088  dissnlocfin  23416  ptval2  23488  dfac14  23505  txdis  23519  xkoptsub  23541  pt1hmeo  23693  xpstopnlem1  23696  tgptsmscls  24037  ustuqtoplem  24127  utopsnneiplem  24135  utopsnneip  24136  utop2nei  24138  utop3cls  24139  pcorev2  24928  pcophtb  24929  pi1grplem  24949  pi1inv  24952  cvsunit  25031  i1f1  25591  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  limcfval  25773  dvnfval  25824  ig1pval  26081  0dgrb  26151  dgrnznn  26152  dgreq0  26171  dgrmulc  26177  plyrem  26213  facth  26214  fta1  26216  aaliou2  26248  taylpfval  26272  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd2lem1  27642  noinfbnd2  27643  addsproplem3  27878  addsuniflem  27908  negsproplem3  27936  negsunif  27961  mulsproplem10  28028  mulsuniflem  28052  n0scut  28226  n0scut2  28227  n0sfincut  28246  zscut  28295  halfcut  28333  addhalfcut  28334  pw2cut  28335  pw2cutp1  28336  zs12bday  28343  axlowdimlem15  28883  axlowdim  28888  1loopgruspgr  29428  1egrvtxdg1r  29438  1egrvtxdg0  29439  wkslem1  29535  wkslem2  29536  iswlk  29538  redwlk  29600  wlkp1lem8  29608  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  loopclwwlkn1b  29971  clwwlkn1loopb  29972  clwwlknon1  30026  eupth2lem3lem3  30159  frgrncvvdeqlem3  30230  frgrncvvdeqlem5  30232  wlkl0  30296  0ofval  30716  fcnvgreu  32597  indval2  32777  chnccats1  32941  cycpm2tr  33076  lindfpropd  33353  nsgqusf1olem1  33384  elrspunidl  33399  qsidomlem2  33424  opprqusdrng  33464  rprmval  33487  isufd  33511  pidufd  33514  r1pquslmic  33576  sradrng  33578  rlmdim  33605  rgmoddimOLD  33606  ply1degltdimlem  33618  dimkerim  33623  lvecendof1f1o  33629  irngval  33680  minplym1p  33703  minplynzm1p  33704  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  dispcmp  33849  ordtprsval  33908  ordtprsuni  33909  sitgval  34323  sseqval  34379  reprsuc  34606  lpadval  34667  bnj941  34762  bnj944  34928  revwlk  35112  subfacp1lem5  35171  sconnpht  35216  sconnpht2  35225  sconnpi1  35226  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift2lem13  35302  cvmlift3lem9  35314  satffunlem1lem1  35389  satffunlem2lem1  35391  msrval  35525  mthmpps  35569  onint1  36437  bj-projeq  36980  bj-restsn  37070  finixpnum  37599  matunitlindflem1  37610  ptrest  37613  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  poimirlem26  37640  grpokerinj  37887  isdivrngo  37944  drngoi  37945  isprrngo  38044  lsatset  38983  lsmsat  39001  islshpat  39010  lflsc0N  39076  lkrfval  39080  ldualset  39118  dvafset  40998  dvaset  40999  dvhfset  41074  dvhset  41075  dibffval  41134  dibfval  41135  dib0  41158  cdlemn4a  41193  dihmeetlem4preN  41300  dihmeetlem13N  41313  dih1dimatlem  41323  dihlsprn  41325  dvh2dim  41439  lpolsetN  41476  lclkrlem2j  41510  lclkrlem2p  41516  lcfrlem21  41557  mapdpglem22  41687  mapdpglem23  41688  mapdpglem26  41692  mapdpglem27  41693  mapdpg  41700  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdindp4  41717  mapdhval  41718  mapdheq  41722  mapdh6aN  41729  hvmapffval  41752  hvmapfval  41753  hvmap1o2  41759  hdmap1fval  41790  hdmap1vallem  41791  hdmap1val  41792  hdmap1eq  41795  hdmap1cbv  41796  hdmap1l6a  41803  hdmapfval  41821  hdmap10  41834  hdmaprnlem6N  41848  hgmaprnlem2N  41891  lcmfunnnd  42000  aks6d1c6lem5  42165  qsalrel  42228  frlmsnic  42528  prjspval  42591  prjspval2  42601  prjspnvs  42608  prjcrvfval  42619  dfac11  43051  dfac21  43055  nzprmdif  44308  expgrowth  44324  fzdifsuc2  45308  cnrefiisplem  45827  cnrefiisp  45828  hoidmv1le  46592  ovnovollem3  46656  fsetsniunop  47050  fsetsnf  47052  fsetsnf1  47053  fsetsnfo  47054  dfateq12d  47127  otiunsndisjX  47280  funop1  47284  preimafvelsetpreimafv  47389  imaelsetpreimafv  47396  imasetpreimafvbijlemfo  47406  fundcmpsurbijinjpreimafv  47408  fundcmpsurinj  47410  fundcmpsurbijinj  47411  lmod1zr  48482  0aryfvalel  48623  1arymaptf1  48631  discsubc  49053  imasubclem3  49095  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  termcbas2  49471  termchom  49477  termchom2  49478  termcfuncval  49521  mndtcval  49568