Theorem sneqd 4585

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

Syntax hints:   → wi 4   = wceq 1541  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-sn 4574

This theorem is referenced by:  eqsnuniex  5297  otsndisj  5457  otiunsndisj  5458  iunopeqop  5459  dmsnopss  6161  dmsnsnsn  6167  opswap  6176  ressn  6232  suceqd  6373  f1osng  6804  fsng  7070  fsn2g  7071  funopsn  7081  funsneqopb  7085  fnressn  7091  2nd1st  7970  dfmpo  8032  cnvf1olem  8040  xpord2pred  8075  xpord3pred  8082  suppsnop  8108  tpostpos  8176  tfrlem11  8307  naddcllem  8591  ralxpmap  8820  elixpsn  8861  ixpsnf1o  8862  en1b  8947  mapsnend  8958  xpassen  8984  dif1en  9071  en1eqsn  9159  cantnfp1lem3  9570  axdc4lem  10346  ttukeylem3  10402  ttukey2g  10407  fpwwe2lem12  10533  fztp  13480  fzsuc2  13482  fseq1p1m1  13498  fseq1m1p1  13499  expval  13970  hash1elsn  14278  s1val  14506  s1eq  14508  s3sndisj  14874  s3iunsndisj  14875  fsumm1  15658  fprodm1  15874  divalgmod  16317  vdwpc  16892  vdwlem1  16893  vdwlem6  16898  vdwlem7  16899  vdwlem8  16900  cshwsdisj  17010  strle1  17069  setsvalg  17077  setsidvald  17110  imasval  17415  imasaddvallem  17433  imasvscaval  17442  ismri2dad  17543  mreexd  17548  mreexmrid  17549  homaval  17938  setcmon  17994  funcsetcestrclem1  18060  chnccats1  18531  chnccat  18532  gsumress  18590  pwsco2mhm  18741  efmnd  18778  idressubmefmnd  18806  smndex1igid  18812  smndex1basss  18813  smndex1mgm  18815  smndex1mndlem  18817  mulgval  18984  idressubgsymg  19322  gsumzaddlem  19833  dmdprd  19912  subgdmdprd  19948  dprdsn  19950  dprd2da  19956  dmdprdpr  19963  dprdpr  19964  dpjfval  19969  dpjval  19970  ablfac1eulem  19986  pgpfaclem1  19995  isunit  20291  isdrng  20648  drngprop  20659  isdrngd  20680  isdrngdOLD  20682  drngpropd  20684  issubdrg  20695  subdrgint  20718  lspsnneg  20939  lspsnsub  20940  lmodindp1  20947  islbs  21010  lspsntrim  21032  lbspropd  21033  lspsnvs  21051  lspsneleq  21052  lspfixed  21065  rngqiprngimf1  21237  lpival  21261  pzriprnglem13  21430  pzriprnglem14  21431  zrhrhmb  21447  znval  21472  isobs  21657  frlmval  21685  frlmlbs  21734  islindf  21749  lindfmm  21764  lsslindf  21767  islindf4  21775  islindf5  21776  psrval  21852  mat1dimmul  22391  mat1dimcrng  22392  mat1rhmval  22394  mat1ric  22402  mat1scmat  22454  mdet0pr  22507  m1detdiag  22512  pmatcoe1fsupp  22616  ordtval  23104  ordtcnv  23116  dissnlocfin  23444  ptval2  23516  dfac14  23533  txdis  23547  xkoptsub  23569  pt1hmeo  23721  xpstopnlem1  23724  tgptsmscls  24065  ustuqtoplem  24154  utopsnneiplem  24162  utopsnneip  24163  utop2nei  24165  utop3cls  24166  pcorev2  24955  pcophtb  24956  pi1grplem  24976  pi1inv  24979  cvsunit  25058  i1f1  25618  i1faddlem  25621  i1fmullem  25622  i1fadd  25623  limcfval  25800  dvnfval  25851  ig1pval  26108  0dgrb  26178  dgrnznn  26179  dgreq0  26198  dgrmulc  26204  plyrem  26240  facth  26241  fta1  26243  aaliou2  26275  taylpfval  26299  nosupbnd2lem1  27654  nosupbnd2  27655  noinfbnd2lem1  27669  noinfbnd2  27670  eqscut3  27765  addsproplem3  27914  addsuniflem  27944  negsproplem3  27972  negsunif  27997  mulsproplem10  28064  mulsuniflem  28088  n0scut  28262  n0scut2  28263  n0sfincut  28282  zscut  28331  halfcut  28378  addhalfcut  28379  pw2cut  28380  pw2cutp1  28381  pw2cut2  28382  zs12bday  28394  axlowdimlem15  28934  axlowdim  28939  1loopgruspgr  29479  1egrvtxdg1r  29489  1egrvtxdg0  29490  wkslem1  29586  wkslem2  29587  iswlk  29589  redwlk  29649  wlkp1lem8  29657  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  crctcshwlkn0lem6  29793  loopclwwlkn1b  30022  clwwlkn1loopb  30023  clwwlknon1  30077  eupth2lem3lem3  30210  frgrncvvdeqlem3  30281  frgrncvvdeqlem5  30283  wlkl0  30347  0ofval  30767  fcnvgreu  32655  indval2  32835  cycpm2tr  33088  lindfpropd  33347  nsgqusf1olem1  33378  elrspunidl  33393  qsidomlem2  33418  opprqusdrng  33458  rprmval  33481  isufd  33505  pidufd  33508  r1pquslmic  33571  sradrng  33594  rlmdim  33622  rgmoddimOLD  33623  ply1degltdimlem  33635  dimkerim  33640  lvecendof1f1o  33646  irngval  33698  extdgfialglem1  33705  minplym1p  33726  minplynzm1p  33727  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  dispcmp  33872  ordtprsval  33931  ordtprsuni  33932  sitgval  34345  sseqval  34401  reprsuc  34628  lpadval  34689  bnj941  34784  bnj944  34950  revwlk  35169  subfacp1lem5  35228  sconnpht  35273  sconnpht2  35282  sconnpi1  35283  cvmliftlem7  35335  cvmliftlem10  35338  cvmlift2lem13  35359  cvmlift3lem9  35371  satffunlem1lem1  35446  satffunlem2lem1  35448  msrval  35582  mthmpps  35626  onint1  36493  bj-projeq  37036  bj-restsn  37126  finixpnum  37655  matunitlindflem1  37666  ptrest  37669  poimirlem4  37674  poimirlem13  37683  poimirlem14  37684  poimirlem16  37686  poimirlem19  37689  poimirlem26  37696  grpokerinj  37943  isdivrngo  38000  drngoi  38001  isprrngo  38100  lsatset  39099  lsmsat  39117  islshpat  39126  lflsc0N  39192  lkrfval  39196  ldualset  39234  dvafset  41113  dvaset  41114  dvhfset  41189  dvhset  41190  dibffval  41249  dibfval  41250  dib0  41273  cdlemn4a  41308  dihmeetlem4preN  41415  dihmeetlem13N  41428  dih1dimatlem  41438  dihlsprn  41440  dvh2dim  41554  lpolsetN  41591  lclkrlem2j  41625  lclkrlem2p  41631  lcfrlem21  41672  mapdpglem22  41802  mapdpglem23  41803  mapdpglem26  41807  mapdpglem27  41808  mapdpg  41815  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  baerlem5amN  41825  baerlem5bmN  41826  baerlem5abmN  41827  mapdindp4  41832  mapdhval  41833  mapdheq  41837  mapdh6aN  41844  hvmapffval  41867  hvmapfval  41868  hvmap1o2  41874  hdmap1fval  41905  hdmap1vallem  41906  hdmap1val  41907  hdmap1eq  41910  hdmap1cbv  41911  hdmap1l6a  41918  hdmapfval  41936  hdmap10  41949  hdmaprnlem6N  41963  hgmaprnlem2N  42006  lcmfunnnd  42115  aks6d1c6lem5  42280  qsalrel  42343  frlmsnic  42643  prjspval  42706  prjspval2  42716  prjspnvs  42723  prjcrvfval  42734  dfac11  43165  dfac21  43169  nzprmdif  44422  expgrowth  44438  fzdifsuc2  45421  cnrefiisplem  45937  cnrefiisp  45938  hoidmv1le  46702  ovnovollem3  46766  fsetsniunop  47159  fsetsnf  47161  fsetsnf1  47162  fsetsnfo  47163  dfateq12d  47236  otiunsndisjX  47389  funop1  47393  preimafvelsetpreimafv  47498  imaelsetpreimafv  47505  imasetpreimafvbijlemfo  47515  fundcmpsurbijinjpreimafv  47517  fundcmpsurinj  47519  fundcmpsurbijinj  47520  lmod1zr  48604  0aryfvalel  48745  1arymaptf1  48753  discsubc  49175  imasubclem3  49217  swapf1a  49380  swapf2a  49382  swapf1  49383  swapf2  49385  termcbas2  49593  termchom  49599  termchom2  49600  termcfuncval  49643  mndtcval  49690