Theorem sneqd 4589

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

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

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-sn 4578

This theorem is referenced by:  eqsnuniex  5303  otsndisj  5464  otiunsndisj  5465  iunopeqop  5466  dmsnopss  6169  dmsnsnsn  6175  opswap  6184  ressn  6240  suceqd  6381  f1osng  6813  fsng  7079  fsn2g  7080  funopsn  7090  funsneqopb  7094  fnressn  7100  2nd1st  7979  dfmpo  8041  cnvf1olem  8049  xpord2pred  8084  xpord3pred  8091  suppsnop  8117  tpostpos  8185  tfrlem11  8316  naddcllem  8600  ralxpmap  8829  elixpsn  8870  ixpsnf1o  8871  en1b  8957  mapsnend  8968  xpassen  8994  dif1en  9081  en1eqsn  9169  cantnfp1lem3  9580  axdc4lem  10356  ttukeylem3  10412  ttukey2g  10417  fpwwe2lem12  10543  fztp  13490  fzsuc2  13492  fseq1p1m1  13508  fseq1m1p1  13509  expval  13980  hash1elsn  14288  s1val  14516  s1eq  14518  s3sndisj  14884  s3iunsndisj  14885  fsumm1  15668  fprodm1  15884  divalgmod  16327  vdwpc  16902  vdwlem1  16903  vdwlem6  16908  vdwlem7  16909  vdwlem8  16910  cshwsdisj  17020  strle1  17079  setsvalg  17087  setsidvald  17120  imasval  17425  imasaddvallem  17443  imasvscaval  17452  ismri2dad  17553  mreexd  17558  mreexmrid  17559  homaval  17948  setcmon  18004  funcsetcestrclem1  18070  chnccats1  18541  chnccat  18542  gsumress  18600  pwsco2mhm  18751  efmnd  18788  idressubmefmnd  18816  smndex1igid  18822  smndex1basss  18823  smndex1mgm  18825  smndex1mndlem  18827  mulgval  18994  idressubgsymg  19332  gsumzaddlem  19843  dmdprd  19922  subgdmdprd  19958  dprdsn  19960  dprd2da  19966  dmdprdpr  19973  dprdpr  19974  dpjfval  19979  dpjval  19980  ablfac1eulem  19996  pgpfaclem1  20005  isunit  20301  isdrng  20658  drngprop  20669  isdrngd  20690  isdrngdOLD  20692  drngpropd  20694  issubdrg  20705  subdrgint  20728  lspsnneg  20949  lspsnsub  20950  lmodindp1  20957  islbs  21020  lspsntrim  21042  lbspropd  21043  lspsnvs  21061  lspsneleq  21062  lspfixed  21075  rngqiprngimf1  21247  lpival  21271  pzriprnglem13  21440  pzriprnglem14  21441  zrhrhmb  21457  znval  21482  isobs  21667  frlmval  21695  frlmlbs  21744  islindf  21759  lindfmm  21774  lsslindf  21777  islindf4  21785  islindf5  21786  psrval  21862  mat1dimmul  22401  mat1dimcrng  22402  mat1rhmval  22404  mat1ric  22412  mat1scmat  22464  mdet0pr  22517  m1detdiag  22522  pmatcoe1fsupp  22626  ordtval  23114  ordtcnv  23126  dissnlocfin  23454  ptval2  23526  dfac14  23543  txdis  23557  xkoptsub  23579  pt1hmeo  23731  xpstopnlem1  23734  tgptsmscls  24075  ustuqtoplem  24164  utopsnneiplem  24172  utopsnneip  24173  utop2nei  24175  utop3cls  24176  pcorev2  24965  pcophtb  24966  pi1grplem  24986  pi1inv  24989  cvsunit  25068  i1f1  25628  i1faddlem  25631  i1fmullem  25632  i1fadd  25633  limcfval  25810  dvnfval  25861  ig1pval  26118  0dgrb  26188  dgrnznn  26189  dgreq0  26208  dgrmulc  26214  plyrem  26250  facth  26251  fta1  26253  aaliou2  26285  taylpfval  26309  nosupbnd2lem1  27664  nosupbnd2  27665  noinfbnd2lem1  27679  noinfbnd2  27680  eqscut3  27775  addsproplem3  27924  addsuniflem  27954  negsproplem3  27982  negsunif  28007  mulsproplem10  28074  mulsuniflem  28098  n0scut  28272  n0scut2  28273  n0sfincut  28292  zscut  28341  halfcut  28388  addhalfcut  28389  pw2cut  28390  pw2cutp1  28391  pw2cut2  28392  zs12bday  28404  axlowdimlem15  28945  axlowdim  28950  1loopgruspgr  29490  1egrvtxdg1r  29500  1egrvtxdg0  29501  wkslem1  29597  wkslem2  29598  iswlk  29600  redwlk  29660  wlkp1lem8  29668  crctcshwlkn0lem4  29802  crctcshwlkn0lem5  29803  crctcshwlkn0lem6  29804  loopclwwlkn1b  30033  clwwlkn1loopb  30034  clwwlknon1  30088  eupth2lem3lem3  30221  frgrncvvdeqlem3  30292  frgrncvvdeqlem5  30294  wlkl0  30358  0ofval  30778  fcnvgreu  32666  indval2  32846  cycpm2tr  33099  lindfpropd  33358  nsgqusf1olem1  33389  elrspunidl  33404  qsidomlem2  33429  opprqusdrng  33469  rprmval  33492  isufd  33516  pidufd  33519  r1pquslmic  33582  sradrng  33605  rlmdim  33633  rgmoddimOLD  33634  ply1degltdimlem  33646  dimkerim  33651  lvecendof1f1o  33657  irngval  33709  extdgfialglem1  33716  minplym1p  33737  minplynzm1p  33738  algextdeglem3  33743  algextdeglem4  33744  algextdeglem5  33745  dispcmp  33883  ordtprsval  33942  ordtprsuni  33943  sitgval  34356  sseqval  34412  reprsuc  34639  lpadval  34700  bnj941  34795  bnj944  34961  revwlk  35180  subfacp1lem5  35239  sconnpht  35284  sconnpht2  35293  sconnpi1  35294  cvmliftlem7  35346  cvmliftlem10  35349  cvmlift2lem13  35370  cvmlift3lem9  35382  satffunlem1lem1  35457  satffunlem2lem1  35459  msrval  35593  mthmpps  35637  onint1  36504  bj-projeq  37047  bj-restsn  37137  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  42348  frlmsnic  42648  prjspval  42711  prjspval2  42721  prjspnvs  42728  prjcrvfval  42739  dfac11  43169  dfac21  43173  nzprmdif  44426  expgrowth  44442  fzdifsuc2  45425  cnrefiisplem  45941  cnrefiisp  45942  hoidmv1le  46706  ovnovollem3  46770  fsetsniunop  47163  fsetsnf  47165  fsetsnf1  47166  fsetsnfo  47167  dfateq12d  47240  otiunsndisjX  47393  funop1  47397  preimafvelsetpreimafv  47502  imaelsetpreimafv  47509  imasetpreimafvbijlemfo  47519  fundcmpsurbijinjpreimafv  47521  fundcmpsurinj  47523  fundcmpsurbijinj  47524  lmod1zr  48608  0aryfvalel  48749  1arymaptf1  48757  discsubc  49179  imasubclem3  49221  swapf1a  49384  swapf2a  49386  swapf1  49387  swapf2  49389  termcbas2  49597  termchom  49603  termchom2  49604  termcfuncval  49647  mndtcval  49694