Theorem sneqd 4579

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-sn 4568

This theorem is referenced by:  eqsnuniex  5303  otsndisj  5473  otiunsndisj  5474  iunopeqop  5475  iunopeqopOLD  5476  dmsnopss  6178  dmsnsnsn  6184  opswap  6193  ressn  6249  suceqd  6390  f1osng  6822  fsng  7090  fsn2g  7091  funopsn  7101  funopsnOLD  7102  funsneqopb  7106  fnressn  7112  2nd1st  7991  dfmpo  8052  cnvf1olem  8060  xpord2pred  8095  xpord3pred  8102  suppsnop  8128  tpostpos  8196  tfrlem11  8327  naddcllem  8612  ralxpmap  8844  elixpsn  8885  ixpsnf1o  8886  en1b  8972  mapsnend  8983  xpassen  9009  dif1en  9096  en1eqsn  9185  cantnfp1lem3  9601  axdc4lem  10377  ttukeylem3  10433  ttukey2g  10438  fpwwe2lem12  10565  indval2  12164  fztp  13534  fzsuc2  13536  fseq1p1m1  13552  fseq1m1p1  13553  expval  14025  hash1elsn  14333  s1val  14561  s1eq  14563  s3sndisj  14929  s3iunsndisj  14930  fsumm1  15713  fprodm1  15932  divalgmod  16375  vdwpc  16951  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  cshwsdisj  17069  strle1  17128  setsvalg  17136  setsidvald  17169  imasval  17475  imasaddvallem  17493  imasvscaval  17502  ismri2dad  17603  mreexd  17608  mreexmrid  17609  homaval  17998  setcmon  18054  funcsetcestrclem1  18120  chnccats1  18591  chnccat  18592  gsumress  18650  pwsco2mhm  18801  efmnd  18838  idressubmefmnd  18866  smndex1igid  18874  smndex1igidOLD  18875  smndex1basss  18876  smndex1mgm  18878  smndex1mndlem  18880  mulgval  19047  idressubgsymg  19385  gsumzaddlem  19896  dmdprd  19975  subgdmdprd  20011  dprdsn  20013  dprd2da  20019  dmdprdpr  20026  dprdpr  20027  dpjfval  20032  dpjval  20033  ablfac1eulem  20049  pgpfaclem1  20058  isunit  20353  isdrng  20710  drngprop  20721  isdrngd  20742  isdrngdOLD  20744  drngpropd  20746  issubdrg  20757  subdrgint  20780  lspsnneg  21001  lspsnsub  21002  lmodindp1  21009  islbs  21071  lspsntrim  21093  lbspropd  21094  lspsnvs  21112  lspsneleq  21113  lspfixed  21126  rngqiprngimf1  21298  lpival  21322  pzriprnglem13  21473  pzriprnglem14  21474  zrhrhmb  21490  znval  21515  isobs  21700  frlmval  21728  frlmlbs  21777  islindf  21792  lindfmm  21807  lsslindf  21810  islindf4  21818  islindf5  21819  psrval  21895  mat1dimmul  22441  mat1dimcrng  22442  mat1rhmval  22444  mat1ric  22452  mat1scmat  22504  mdet0pr  22557  m1detdiag  22562  pmatcoe1fsupp  22666  ordtval  23154  ordtcnv  23166  dissnlocfin  23494  ptval2  23566  dfac14  23583  txdis  23597  xkoptsub  23619  pt1hmeo  23771  xpstopnlem1  23774  tgptsmscls  24115  ustuqtoplem  24204  utopsnneiplem  24212  utopsnneip  24213  utop2nei  24215  utop3cls  24216  pcorev2  24995  pcophtb  24996  pi1grplem  25016  pi1inv  25019  cvsunit  25098  i1f1  25657  i1faddlem  25660  i1fmullem  25661  i1fadd  25662  limcfval  25839  dvnfval  25889  ig1pval  26141  0dgrb  26211  dgrnznn  26212  dgreq0  26230  dgrmulc  26236  plyrem  26271  facth  26272  fta1  26274  aaliou2  26306  taylpfval  26330  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noinfbnd2  27695  eqcuts3  27796  addsproplem3  27963  addsuniflem  27993  negsproplem3  28022  negsunif  28047  mulsproplem10  28117  mulsuniflem  28141  n0cut  28326  n0cut2  28327  n0fincut  28347  zcuts  28399  halfcut  28450  addhalfcut  28451  pw2cut  28452  pw2cutp1  28453  pw2cut2  28454  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  elreno2  28487  axlowdimlem15  29025  axlowdim  29030  1loopgruspgr  29569  1egrvtxdg1r  29579  1egrvtxdg0  29580  wkslem1  29676  wkslem2  29677  iswlk  29679  redwlk  29739  wlkp1lem8  29747  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  loopclwwlkn1b  30112  clwwlkn1loopb  30113  clwwlknon1  30167  eupth2lem3lem3  30300  frgrncvvdeqlem3  30371  frgrncvvdeqlem5  30373  wlkl0  30437  0ofval  30858  fresunsn  32698  fcnvgreu  32745  cycpm2tr  33180  lindfpropd  33442  nsgqusf1olem1  33473  elrspunidl  33488  qsidomlem2  33513  opprqusdrng  33553  rprmval  33576  isufd  33600  pidufd  33603  r1pquslmic  33671  extvfvcl  33680  esplyfval0  33708  esplyfval2  33709  esplyind  33719  vieta  33724  sradrng  33726  rlmdim  33754  ply1degltdimlem  33766  dimkerim  33771  lvecendof1f1o  33777  irngval  33829  extdgfialglem1  33836  minplym1p  33857  minplynzm1p  33858  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  dispcmp  34003  ordtprsval  34062  ordtprsuni  34063  sitgval  34476  sseqval  34532  reprsuc  34759  lpadval  34820  bnj941  34915  bnj944  35080  revwlk  35307  subfacp1lem5  35366  sconnpht  35411  sconnpht2  35420  sconnpi1  35421  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift2lem13  35497  cvmlift3lem9  35509  satffunlem1lem1  35584  satffunlem2lem1  35586  msrval  35720  mthmpps  35764  onint1  36631  bj-projeq  37299  bj-restsn  37394  finixpnum  37926  matunitlindflem1  37937  ptrest  37940  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  poimirlem26  37967  grpokerinj  38214  isdivrngo  38271  drngoi  38272  isprrngo  38371  lsatset  39436  lsmsat  39454  islshpat  39463  lflsc0N  39529  lkrfval  39533  ldualset  39571  dvafset  41450  dvaset  41451  dvhfset  41526  dvhset  41527  dibffval  41586  dibfval  41587  dib0  41610  cdlemn4a  41645  dihmeetlem4preN  41752  dihmeetlem13N  41765  dih1dimatlem  41775  dihlsprn  41777  dvh2dim  41891  lpolsetN  41928  lclkrlem2j  41962  lclkrlem2p  41968  lcfrlem21  42009  mapdpglem22  42139  mapdpglem23  42140  mapdpglem26  42144  mapdpglem27  42145  mapdpg  42152  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdindp4  42169  mapdhval  42170  mapdheq  42174  mapdh6aN  42181  hvmapffval  42204  hvmapfval  42205  hvmap1o2  42211  hdmap1fval  42242  hdmap1vallem  42243  hdmap1val  42244  hdmap1eq  42247  hdmap1cbv  42248  hdmap1l6a  42255  hdmapfval  42273  hdmap10  42286  hdmaprnlem6N  42300  hgmaprnlem2N  42343  lcmfunnnd  42451  aks6d1c6lem5  42616  qsalrel  42680  frlmsnic  42985  prjspval  43036  prjspval2  43046  prjspnvs  43053  prjcrvfval  43064  dfac11  43490  dfac21  43494  nzprmdif  44746  expgrowth  44762  fzdifsuc2  45743  cnrefiisplem  46257  cnrefiisp  46258  hoidmv1le  47022  ovnovollem3  47086  fsetsniunop  47497  fsetsnf  47499  fsetsnf1  47500  fsetsnfo  47501  dfateq12d  47574  otiunsndisjX  47727  funop1  47731  preimafvelsetpreimafv  47848  imaelsetpreimafv  47855  imasetpreimafvbijlemfo  47865  fundcmpsurbijinjpreimafv  47867  fundcmpsurinj  47869  fundcmpsurbijinj  47870  lmod1zr  48969  0aryfvalel  49110  1arymaptf1  49118  discsubc  49539  imasubclem3  49581  swapf1a  49744  swapf2a  49746  swapf1  49747  swapf2  49749  termcbas2  49957  termchom  49963  termchom2  49964  termcfuncval  50007  mndtcval  50054