Theorem sneqd 4580

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4569

This theorem is referenced by:  eqsnuniex  5299  otsndisj  5468  otiunsndisj  5469  iunopeqop  5470  dmsnopss  6173  dmsnsnsn  6179  opswap  6188  ressn  6244  suceqd  6385  f1osng  6817  fsng  7085  fsn2g  7086  funopsn  7096  funsneqopb  7100  fnressn  7106  2nd1st  7985  dfmpo  8046  cnvf1olem  8054  xpord2pred  8089  xpord3pred  8096  suppsnop  8122  tpostpos  8190  tfrlem11  8321  naddcllem  8606  ralxpmap  8838  elixpsn  8879  ixpsnf1o  8880  en1b  8966  mapsnend  8977  xpassen  9003  dif1en  9090  en1eqsn  9179  cantnfp1lem3  9595  axdc4lem  10371  ttukeylem3  10427  ttukey2g  10432  fpwwe2lem12  10559  indval2  12158  fztp  13528  fzsuc2  13530  fseq1p1m1  13546  fseq1m1p1  13547  expval  14019  hash1elsn  14327  s1val  14555  s1eq  14557  s3sndisj  14923  s3iunsndisj  14924  fsumm1  15707  fprodm1  15926  divalgmod  16369  vdwpc  16945  vdwlem1  16946  vdwlem6  16951  vdwlem7  16952  vdwlem8  16953  cshwsdisj  17063  strle1  17122  setsvalg  17130  setsidvald  17163  imasval  17469  imasaddvallem  17487  imasvscaval  17496  ismri2dad  17597  mreexd  17602  mreexmrid  17603  homaval  17992  setcmon  18048  funcsetcestrclem1  18114  chnccats1  18585  chnccat  18586  gsumress  18644  pwsco2mhm  18795  efmnd  18832  idressubmefmnd  18860  smndex1igid  18868  smndex1igidOLD  18869  smndex1basss  18870  smndex1mgm  18872  smndex1mndlem  18874  mulgval  19041  idressubgsymg  19379  gsumzaddlem  19890  dmdprd  19969  subgdmdprd  20005  dprdsn  20007  dprd2da  20013  dmdprdpr  20020  dprdpr  20021  dpjfval  20026  dpjval  20027  ablfac1eulem  20043  pgpfaclem1  20052  isunit  20347  isdrng  20704  drngprop  20715  isdrngd  20736  isdrngdOLD  20738  drngpropd  20740  issubdrg  20751  subdrgint  20774  lspsnneg  20995  lspsnsub  20996  lmodindp1  21003  islbs  21066  lspsntrim  21088  lbspropd  21089  lspsnvs  21107  lspsneleq  21108  lspfixed  21121  rngqiprngimf1  21293  lpival  21317  pzriprnglem13  21486  pzriprnglem14  21487  zrhrhmb  21503  znval  21528  isobs  21713  frlmval  21741  frlmlbs  21790  islindf  21805  lindfmm  21820  lsslindf  21823  islindf4  21831  islindf5  21832  psrval  21908  mat1dimmul  22454  mat1dimcrng  22455  mat1rhmval  22457  mat1ric  22465  mat1scmat  22517  mdet0pr  22570  m1detdiag  22575  pmatcoe1fsupp  22679  ordtval  23167  ordtcnv  23179  dissnlocfin  23507  ptval2  23579  dfac14  23596  txdis  23610  xkoptsub  23632  pt1hmeo  23784  xpstopnlem1  23787  tgptsmscls  24128  ustuqtoplem  24217  utopsnneiplem  24225  utopsnneip  24226  utop2nei  24228  utop3cls  24229  pcorev2  25008  pcophtb  25009  pi1grplem  25029  pi1inv  25032  cvsunit  25111  i1f1  25670  i1faddlem  25673  i1fmullem  25674  i1fadd  25675  limcfval  25852  dvnfval  25902  ig1pval  26154  0dgrb  26224  dgrnznn  26225  dgreq0  26243  dgrmulc  26249  plyrem  26285  facth  26286  fta1  26288  aaliou2  26320  taylpfval  26344  nosupbnd2lem1  27696  nosupbnd2  27697  noinfbnd2lem1  27711  noinfbnd2  27712  eqcuts3  27813  addsproplem3  27980  addsuniflem  28010  negsproplem3  28039  negsunif  28064  mulsproplem10  28134  mulsuniflem  28158  n0cut  28343  n0cut2  28344  n0fincut  28364  zcuts  28416  halfcut  28467  addhalfcut  28468  pw2cut  28469  pw2cutp1  28470  pw2cut2  28471  bdaypw2n0bndlem  28472  bdayfinbndlem1  28476  elreno2  28504  axlowdimlem15  29042  axlowdim  29047  1loopgruspgr  29587  1egrvtxdg1r  29597  1egrvtxdg0  29598  wkslem1  29694  wkslem2  29695  iswlk  29697  redwlk  29757  wlkp1lem8  29765  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  loopclwwlkn1b  30130  clwwlkn1loopb  30131  clwwlknon1  30185  eupth2lem3lem3  30318  frgrncvvdeqlem3  30389  frgrncvvdeqlem5  30391  wlkl0  30455  0ofval  30876  fresunsn  32716  fcnvgreu  32763  cycpm2tr  33198  lindfpropd  33460  nsgqusf1olem1  33491  elrspunidl  33506  qsidomlem2  33531  opprqusdrng  33571  rprmval  33594  isufd  33618  pidufd  33621  r1pquslmic  33689  extvfvcl  33698  esplyfval0  33726  esplyfval2  33727  esplyind  33737  vieta  33742  sradrng  33744  rlmdim  33772  rgmoddimOLD  33773  ply1degltdimlem  33785  dimkerim  33790  lvecendof1f1o  33796  irngval  33848  extdgfialglem1  33855  minplym1p  33876  minplynzm1p  33877  algextdeglem3  33882  algextdeglem4  33883  algextdeglem5  33884  dispcmp  34022  ordtprsval  34081  ordtprsuni  34082  sitgval  34495  sseqval  34551  reprsuc  34778  lpadval  34839  bnj941  34934  bnj944  35099  revwlk  35326  subfacp1lem5  35385  sconnpht  35430  sconnpht2  35439  sconnpi1  35440  cvmliftlem7  35492  cvmliftlem10  35495  cvmlift2lem13  35516  cvmlift3lem9  35528  satffunlem1lem1  35603  satffunlem2lem1  35605  msrval  35739  mthmpps  35783  onint1  36650  bj-projeq  37318  bj-restsn  37413  finixpnum  37943  matunitlindflem1  37954  ptrest  37957  poimirlem4  37962  poimirlem13  37971  poimirlem14  37972  poimirlem16  37974  poimirlem19  37977  poimirlem26  37984  grpokerinj  38231  isdivrngo  38288  drngoi  38289  isprrngo  38388  lsatset  39453  lsmsat  39471  islshpat  39480  lflsc0N  39546  lkrfval  39550  ldualset  39588  dvafset  41467  dvaset  41468  dvhfset  41543  dvhset  41544  dibffval  41603  dibfval  41604  dib0  41627  cdlemn4a  41662  dihmeetlem4preN  41769  dihmeetlem13N  41782  dih1dimatlem  41792  dihlsprn  41794  dvh2dim  41908  lpolsetN  41945  lclkrlem2j  41979  lclkrlem2p  41985  lcfrlem21  42026  mapdpglem22  42156  mapdpglem23  42157  mapdpglem26  42161  mapdpglem27  42162  mapdpg  42169  baerlem3lem2  42173  baerlem5alem2  42174  baerlem5blem2  42175  baerlem5amN  42179  baerlem5bmN  42180  baerlem5abmN  42181  mapdindp4  42186  mapdhval  42187  mapdheq  42191  mapdh6aN  42198  hvmapffval  42221  hvmapfval  42222  hvmap1o2  42228  hdmap1fval  42259  hdmap1vallem  42260  hdmap1val  42261  hdmap1eq  42264  hdmap1cbv  42265  hdmap1l6a  42272  hdmapfval  42290  hdmap10  42303  hdmaprnlem6N  42317  hgmaprnlem2N  42360  lcmfunnnd  42468  aks6d1c6lem5  42633  qsalrel  42697  frlmsnic  43002  prjspval  43053  prjspval2  43063  prjspnvs  43070  prjcrvfval  43081  dfac11  43511  dfac21  43515  nzprmdif  44767  expgrowth  44783  fzdifsuc2  45764  cnrefiisplem  46278  cnrefiisp  46279  hoidmv1le  47043  ovnovollem3  47107  fsetsniunop  47512  fsetsnf  47514  fsetsnf1  47515  fsetsnfo  47516  dfateq12d  47589  otiunsndisjX  47742  funop1  47746  preimafvelsetpreimafv  47863  imaelsetpreimafv  47870  imasetpreimafvbijlemfo  47880  fundcmpsurbijinjpreimafv  47882  fundcmpsurinj  47884  fundcmpsurbijinj  47885  lmod1zr  48984  0aryfvalel  49125  1arymaptf1  49133  discsubc  49554  imasubclem3  49596  swapf1a  49759  swapf2a  49761  swapf1  49762  swapf2  49764  termcbas2  49972  termchom  49978  termchom2  49979  termcfuncval  50022  mndtcval  50069