Theorem sneqd 4620

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 4618	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1539  {csn 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-sn 4609

This theorem is referenced by:  eqsnuniex  5343  otsndisj  5506  otiunsndisj  5507  iunopeqop  5508  dmsnopss  6216  dmsnsnsn  6222  opswap  6231  ressn  6287  f1osng  6870  fsng  7138  fsn2g  7139  funopsn  7149  funsneqopb  7153  fnressn  7159  2nd1st  8046  dfmpo  8110  cnvf1olem  8118  xpord2pred  8153  xpord3pred  8160  suppsnop  8186  tpostpos  8254  tfrlem11  8411  naddcllem  8697  ralxpmap  8919  elixpsn  8960  ixpsnf1o  8961  en1b  9048  mapsnend  9059  xpassen  9089  dif1en  9183  dif1enOLD  9185  en1eqsn  9291  cantnfp1lem3  9703  axdc4lem  10478  ttukeylem3  10534  ttukey2g  10539  fpwwe2lem12  10665  fztp  13603  fzsuc2  13605  fseq1p1m1  13621  fseq1m1p1  13622  expval  14087  hash1elsn  14393  s1val  14619  s1eq  14621  s3sndisj  14989  s3iunsndisj  14990  fsumm1  15770  fprodm1  15986  divalgmod  16426  vdwpc  17001  vdwlem1  17002  vdwlem6  17007  vdwlem7  17008  vdwlem8  17009  cshwsdisj  17119  strle1  17178  setsvalg  17186  setsidvald  17219  imasval  17532  imasaddvallem  17550  imasvscaval  17559  ismri2dad  17656  mreexd  17661  mreexmrid  17662  homaval  18052  setcmon  18108  funcsetcestrclem1  18174  gsumress  18669  pwsco2mhm  18820  efmnd  18857  idressubmefmnd  18885  smndex1igid  18891  smndex1basss  18892  smndex1mgm  18894  smndex1mndlem  18896  mulgval  19063  idressubgsymg  19401  gsumzaddlem  19912  dmdprd  19991  subgdmdprd  20027  dprdsn  20029  dprd2da  20035  dmdprdpr  20042  dprdpr  20043  dpjfval  20048  dpjval  20049  ablfac1eulem  20065  pgpfaclem1  20074  isunit  20346  isdrng  20706  drngprop  20717  isdrngd  20738  isdrngdOLD  20740  drngpropd  20742  issubdrg  20754  subdrgint  20777  lspsnneg  20977  lspsnsub  20978  lmodindp1  20985  islbs  21048  lspsntrim  21070  lbspropd  21071  lspsnvs  21089  lspsneleq  21090  lspfixed  21103  rngqiprngimf1  21277  lpival  21301  pzriprnglem13  21471  pzriprnglem14  21472  zrhrhmb  21488  znval  21517  isobs  21707  frlmval  21735  frlmlbs  21784  islindf  21799  lindfmm  21814  lsslindf  21817  islindf4  21825  islindf5  21826  psrval  21902  mat1dimmul  22449  mat1dimcrng  22450  mat1rhmval  22452  mat1ric  22460  mat1scmat  22512  mdet0pr  22565  m1detdiag  22570  pmatcoe1fsupp  22674  ordtval  23162  ordtcnv  23174  dissnlocfin  23502  ptval2  23574  dfac14  23591  txdis  23605  xkoptsub  23627  pt1hmeo  23779  xpstopnlem1  23782  tgptsmscls  24123  ustuqtoplem  24213  utopsnneiplem  24221  utopsnneip  24222  utop2nei  24224  utop3cls  24225  pcorev2  25016  pcophtb  25017  pi1grplem  25037  pi1inv  25040  cvsunit  25119  i1f1  25680  i1faddlem  25683  i1fmullem  25684  i1fadd  25685  limcfval  25862  dvnfval  25913  ig1pval  26170  0dgrb  26240  dgrnznn  26241  dgreq0  26260  dgrmulc  26266  plyrem  26302  facth  26303  fta1  26305  aaliou2  26337  taylpfval  26361  nosupbnd2lem1  27715  nosupbnd2  27716  noinfbnd2lem1  27730  noinfbnd2  27731  addsproplem3  27959  addsuniflem  27989  negsproplem3  28017  negsunif  28042  mulsproplem10  28106  mulsuniflem  28130  n0scut  28293  n0sbday  28309  zscut  28348  halfcut  28371  cutpw2  28372  addhalfcut  28374  pw2cut  28375  zs12bday  28379  axlowdimlem15  28920  axlowdim  28925  1loopgruspgr  29465  1egrvtxdg1r  29475  1egrvtxdg0  29476  wkslem1  29572  wkslem2  29573  iswlk  29575  redwlk  29637  wlkp1lem8  29645  crctcshwlkn0lem4  29780  crctcshwlkn0lem5  29781  crctcshwlkn0lem6  29782  loopclwwlkn1b  30008  clwwlkn1loopb  30009  clwwlknon1  30063  eupth2lem3lem3  30196  frgrncvvdeqlem3  30267  frgrncvvdeqlem5  30269  wlkl0  30333  0ofval  30753  fcnvgreu  32630  indval2  32786  chnccats1  32951  cycpm2tr  33085  lindfpropd  33351  nsgqusf1olem1  33382  elrspunidl  33397  qsidomlem2  33422  opprqusdrng  33462  rprmval  33485  isufd  33509  pidufd  33512  r1pquslmic  33572  sradrng  33574  rlmdim  33601  rgmoddimOLD  33602  ply1degltdimlem  33614  dimkerim  33619  lvecendof1f1o  33625  irngval  33676  minplym1p  33697  algextdeglem3  33701  algextdeglem4  33702  algextdeglem5  33703  dispcmp  33799  ordtprsval  33858  ordtprsuni  33859  sitgval  34275  sseqval  34331  reprsuc  34571  lpadval  34632  bnj941  34727  bnj944  34893  revwlk  35071  subfacp1lem5  35130  sconnpht  35175  sconnpht2  35184  sconnpi1  35185  cvmliftlem7  35237  cvmliftlem10  35240  cvmlift2lem13  35261  cvmlift3lem9  35273  satffunlem1lem1  35348  satffunlem2lem1  35350  msrval  35484  mthmpps  35528  onint1  36391  bj-projeq  36934  bj-restsn  37024  finixpnum  37553  matunitlindflem1  37564  ptrest  37567  poimirlem4  37572  poimirlem13  37581  poimirlem14  37582  poimirlem16  37584  poimirlem19  37587  poimirlem26  37594  grpokerinj  37841  isdivrngo  37898  drngoi  37899  isprrngo  37998  lsatset  38932  lsmsat  38950  islshpat  38959  lflsc0N  39025  lkrfval  39029  ldualset  39067  dvafset  40947  dvaset  40948  dvhfset  41023  dvhset  41024  dibffval  41083  dibfval  41084  dib0  41107  cdlemn4a  41142  dihmeetlem4preN  41249  dihmeetlem13N  41262  dih1dimatlem  41272  dihlsprn  41274  dvh2dim  41388  lpolsetN  41425  lclkrlem2j  41459  lclkrlem2p  41465  lcfrlem21  41506  mapdpglem22  41636  mapdpglem23  41637  mapdpglem26  41641  mapdpglem27  41642  mapdpg  41649  baerlem3lem2  41653  baerlem5alem2  41654  baerlem5blem2  41655  baerlem5amN  41659  baerlem5bmN  41660  baerlem5abmN  41661  mapdindp4  41666  mapdhval  41667  mapdheq  41671  mapdh6aN  41678  hvmapffval  41701  hvmapfval  41702  hvmap1o2  41708  hdmap1fval  41739  hdmap1vallem  41740  hdmap1val  41741  hdmap1eq  41744  hdmap1cbv  41745  hdmap1l6a  41752  hdmapfval  41770  hdmap10  41783  hdmaprnlem6N  41797  hgmaprnlem2N  41840  lcmfunnnd  41954  aks6d1c6lem5  42119  qsalrel  42221  frlmsnic  42495  prjspval  42558  prjspval2  42568  prjspnvs  42575  prjcrvfval  42586  dfac11  43019  dfac21  43023  nzprmdif  44283  expgrowth  44299  fzdifsuc2  45267  cnrefiisplem  45789  cnrefiisp  45790  hoidmv1le  46554  ovnovollem3  46618  fsetsniunop  47007  fsetsnf  47009  fsetsnf1  47010  fsetsnfo  47011  dfateq12d  47084  otiunsndisjX  47237  funop1  47241  preimafvelsetpreimafv  47321  imaelsetpreimafv  47328  imasetpreimafvbijlemfo  47338  fundcmpsurbijinjpreimafv  47340  fundcmpsurinj  47342  fundcmpsurbijinj  47343  lmod1zr  48356  0aryfvalel  48501  1arymaptf1  48509  swapf1a  48934  swapf2a  48936  swapf1  48937  swapf2  48939  termcbas2  49094  termchom  49100  termchom2  49101  termcfuncval  49131  mndtcval  49172