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 1540  {csn 4577

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 4578

This theorem is referenced by:  eqsnuniex  5300  otsndisj  5462  otiunsndisj  5463  iunopeqop  5464  dmsnopss  6163  dmsnsnsn  6169  opswap  6178  ressn  6233  suceqd  6374  f1osng  6805  fsng  7071  fsn2g  7072  funopsn  7082  funsneqopb  7086  fnressn  7092  2nd1st  7973  dfmpo  8035  cnvf1olem  8043  xpord2pred  8078  xpord3pred  8085  suppsnop  8111  tpostpos  8179  tfrlem11  8310  naddcllem  8594  ralxpmap  8823  elixpsn  8864  ixpsnf1o  8865  en1b  8950  mapsnend  8961  xpassen  8988  dif1en  9075  en1eqsn  9164  cantnfp1lem3  9576  axdc4lem  10349  ttukeylem3  10405  ttukey2g  10410  fpwwe2lem12  10536  fztp  13483  fzsuc2  13485  fseq1p1m1  13501  fseq1m1p1  13502  expval  13970  hash1elsn  14278  s1val  14505  s1eq  14507  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  gsumress  18556  pwsco2mhm  18707  efmnd  18744  idressubmefmnd  18772  smndex1igid  18778  smndex1basss  18779  smndex1mgm  18781  smndex1mndlem  18783  mulgval  18950  idressubgsymg  19289  gsumzaddlem  19800  dmdprd  19879  subgdmdprd  19915  dprdsn  19917  dprd2da  19923  dmdprdpr  19930  dprdpr  19931  dpjfval  19936  dpjval  19937  ablfac1eulem  19953  pgpfaclem1  19962  isunit  20258  isdrng  20618  drngprop  20629  isdrngd  20650  isdrngdOLD  20652  drngpropd  20654  issubdrg  20665  subdrgint  20688  lspsnneg  20909  lspsnsub  20910  lmodindp1  20917  islbs  20980  lspsntrim  21002  lbspropd  21003  lspsnvs  21021  lspsneleq  21022  lspfixed  21035  rngqiprngimf1  21207  lpival  21231  pzriprnglem13  21400  pzriprnglem14  21401  zrhrhmb  21417  znval  21442  isobs  21627  frlmval  21655  frlmlbs  21704  islindf  21719  lindfmm  21734  lsslindf  21737  islindf4  21745  islindf5  21746  psrval  21822  mat1dimmul  22361  mat1dimcrng  22362  mat1rhmval  22364  mat1ric  22372  mat1scmat  22424  mdet0pr  22477  m1detdiag  22482  pmatcoe1fsupp  22586  ordtval  23074  ordtcnv  23086  dissnlocfin  23414  ptval2  23486  dfac14  23503  txdis  23517  xkoptsub  23539  pt1hmeo  23691  xpstopnlem1  23694  tgptsmscls  24035  ustuqtoplem  24125  utopsnneiplem  24133  utopsnneip  24134  utop2nei  24136  utop3cls  24137  pcorev2  24926  pcophtb  24927  pi1grplem  24947  pi1inv  24950  cvsunit  25029  i1f1  25589  i1faddlem  25592  i1fmullem  25593  i1fadd  25594  limcfval  25771  dvnfval  25822  ig1pval  26079  0dgrb  26149  dgrnznn  26150  dgreq0  26169  dgrmulc  26175  plyrem  26211  facth  26212  fta1  26214  aaliou2  26246  taylpfval  26270  nosupbnd2lem1  27625  nosupbnd2  27626  noinfbnd2lem1  27640  noinfbnd2  27641  eqscut3  27735  addsproplem3  27883  addsuniflem  27913  negsproplem3  27941  negsunif  27966  mulsproplem10  28033  mulsuniflem  28057  n0scut  28231  n0scut2  28232  n0sfincut  28251  zscut  28300  halfcut  28346  addhalfcut  28347  pw2cut  28348  pw2cutp1  28349  zs12bday  28361  axlowdimlem15  28901  axlowdim  28906  1loopgruspgr  29446  1egrvtxdg1r  29456  1egrvtxdg0  29457  wkslem1  29553  wkslem2  29554  iswlk  29556  redwlk  29616  wlkp1lem8  29624  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  crctcshwlkn0lem6  29760  loopclwwlkn1b  29986  clwwlkn1loopb  29987  clwwlknon1  30041  eupth2lem3lem3  30174  frgrncvvdeqlem3  30245  frgrncvvdeqlem5  30247  wlkl0  30311  0ofval  30731  fcnvgreu  32616  indval2  32797  chnccats1  32957  cycpm2tr  33061  lindfpropd  33319  nsgqusf1olem1  33350  elrspunidl  33365  qsidomlem2  33390  opprqusdrng  33430  rprmval  33453  isufd  33477  pidufd  33480  r1pquslmic  33543  sradrng  33548  rlmdim  33576  rgmoddimOLD  33577  ply1degltdimlem  33589  dimkerim  33594  lvecendof1f1o  33600  irngval  33652  extdgfialglem1  33659  minplym1p  33680  minplynzm1p  33681  algextdeglem3  33686  algextdeglem4  33687  algextdeglem5  33688  dispcmp  33826  ordtprsval  33885  ordtprsuni  33886  sitgval  34300  sseqval  34356  reprsuc  34583  lpadval  34644  bnj941  34739  bnj944  34905  revwlk  35098  subfacp1lem5  35157  sconnpht  35202  sconnpht2  35211  sconnpi1  35212  cvmliftlem7  35264  cvmliftlem10  35267  cvmlift2lem13  35288  cvmlift3lem9  35300  satffunlem1lem1  35375  satffunlem2lem1  35377  msrval  35511  mthmpps  35555  onint1  36423  bj-projeq  36966  bj-restsn  37056  finixpnum  37585  matunitlindflem1  37596  ptrest  37599  poimirlem4  37604  poimirlem13  37613  poimirlem14  37614  poimirlem16  37616  poimirlem19  37619  poimirlem26  37626  grpokerinj  37873  isdivrngo  37930  drngoi  37931  isprrngo  38030  lsatset  38969  lsmsat  38987  islshpat  38996  lflsc0N  39062  lkrfval  39066  ldualset  39104  dvafset  40983  dvaset  40984  dvhfset  41059  dvhset  41060  dibffval  41119  dibfval  41120  dib0  41143  cdlemn4a  41178  dihmeetlem4preN  41285  dihmeetlem13N  41298  dih1dimatlem  41308  dihlsprn  41310  dvh2dim  41424  lpolsetN  41461  lclkrlem2j  41495  lclkrlem2p  41501  lcfrlem21  41542  mapdpglem22  41672  mapdpglem23  41673  mapdpglem26  41677  mapdpglem27  41678  mapdpg  41685  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  mapdindp4  41702  mapdhval  41703  mapdheq  41707  mapdh6aN  41714  hvmapffval  41737  hvmapfval  41738  hvmap1o2  41744  hdmap1fval  41775  hdmap1vallem  41776  hdmap1val  41777  hdmap1eq  41780  hdmap1cbv  41781  hdmap1l6a  41788  hdmapfval  41806  hdmap10  41819  hdmaprnlem6N  41833  hgmaprnlem2N  41876  lcmfunnnd  41985  aks6d1c6lem5  42150  qsalrel  42213  frlmsnic  42513  prjspval  42576  prjspval2  42586  prjspnvs  42593  prjcrvfval  42604  dfac11  43035  dfac21  43039  nzprmdif  44292  expgrowth  44308  fzdifsuc2  45292  cnrefiisplem  45810  cnrefiisp  45811  hoidmv1le  46575  ovnovollem3  46639  fsetsniunop  47033  fsetsnf  47035  fsetsnf1  47036  fsetsnfo  47037  dfateq12d  47110  otiunsndisjX  47263  funop1  47267  preimafvelsetpreimafv  47372  imaelsetpreimafv  47379  imasetpreimafvbijlemfo  47389  fundcmpsurbijinjpreimafv  47391  fundcmpsurinj  47393  fundcmpsurbijinj  47394  lmod1zr  48478  0aryfvalel  48619  1arymaptf1  48627  discsubc  49049  imasubclem3  49091  swapf1a  49254  swapf2a  49256  swapf1  49257  swapf2  49259  termcbas2  49467  termchom  49473  termchom2  49474  termcfuncval  49517  mndtcval  49564