Theorem sneqd 4606

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

Syntax hints:   → wi 4   = wceq 1567  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-sn 4595

This theorem is referenced by:  eqsnuniex  5333  otsndisj  5503  otiunsndisj  5504  iunopeqop  5505  iunopeqopOLD  5506  dmsnopss  6216  dmsnsnsn  6222  opswap  6231  ressn  6287  suceqd  6429  f1osng  6864  fsng  7134  fsn2g  7135  funopsn  7145  funopsnOLD  7146  funsneqopb  7150  fnressn  7156  2nd1st  8034  dfmpo  8096  cnvf1olem  8104  xpord2pred  8140  xpord3pred  8147  suppsnop  8173  tpostpos  8241  tfrlem11  8374  naddcllem  8661  ralxpmap  8893  elixpsn  8934  ixpsnf1o  8935  en1b  9021  mapsnend  9032  xpassen  9058  dif1en  9145  en1eqsn  9234  cantnfp1lem3  9648  axdc4lem  10438  ttukeylem3  10494  ttukey2g  10499  fpwwe2lem12  10626  indval2  12222  fztp  13607  fzsuc2  13609  fseq1p1m1  13625  fseq1m1p1  13626  expval  14098  hash1elsn  14406  s1val  14635  s1eq  14637  s3sndisj  15003  s3iunsndisj  15004  fsumm1  15801  fprodm1  16020  divalgmod  16463  vdwpc  17039  vdwlem1  17040  vdwlem6  17045  vdwlem7  17046  vdwlem8  17047  cshwsdisj  17157  strle1  17217  setsvalg  17225  setsidvald  17258  imasval  17564  imasaddvallem  17582  imasvscaval  17591  ismri2dad  17692  mreexd  17697  mreexmrid  17698  homaval  18087  setcmon  18143  funcsetcestrclem1  18209  chnccats1  18680  chnccat  18681  gsumress  18739  pwsco2mhm  18891  efmnd  18928  idressubmefmnd  18956  smndex1igid  18964  smndex1igidOLD  18965  smndex1basss  18966  smndex1mgm  18968  smndex1mndlem  18970  mulgval  19136  idressubgsymg  19479  gsumzaddlem  19990  dmdprd  20069  subgdmdprd  20105  dprdsn  20107  dprd2da  20113  dmdprdpr  20120  dprdpr  20121  dpjfval  20126  dpjval  20127  ablfac1eulem  20143  pgpfaclem1  20152  isunit  20454  isdrng  20816  drngprop  20827  isdrngd  20846  isdrngdOLD  20848  drngpropd  20850  issubdrg  20860  subdrgint  20883  lspsnneg  21104  lspsnsub  21105  lmodindp1  21112  islbs  21174  lspsntrim  21196  lbspropd  21197  lspsnvs  21215  lspsneleq  21216  lspfixed  21229  rngqiprngimf1  21410  qsidomlem2  21449  lpival  21460  pzriprnglem13  21611  pzriprnglem14  21612  zrhrhmb  21628  znval  21653  isobs  21838  frlmval  21866  frlmlbs  21915  islindf  21930  lindfmm  21945  lsslindf  21948  islindf4  21956  islindf5  21957  psrval  22033  mat1dimmul  22601  mat1dimcrng  22602  mat1rhmval  22604  mat1ric  22612  mat1scmat  22664  mdet0pr  22717  m1detdiag  22722  pmatcoe1fsupp  22826  ordtval  23314  ordtcnv  23326  dissnlocfin  23654  ptval2  23726  dfac14  23743  txdis  23757  xkoptsub  23779  pt1hmeo  23931  xpstopnlem1  23934  tgptsmscls  24275  ustuqtoplem  24364  utopsnneiplem  24372  utopsnneip  24373  utop2nei  24375  utop3cls  24376  pcorev2  25155  pcophtb  25156  pi1grplem  25176  pi1inv  25179  cvsunit  25258  i1f1  25817  i1faddlem  25820  i1fmullem  25821  i1fadd  25822  limcfval  25999  dvnfval  26049  ig1pval  26301  0dgrb  26371  dgrnznn  26372  dgreq0  26390  dgrmulc  26396  plyrem  26434  facth  26435  fta1  26437  aaliou2  26469  taylpfval  26493  nosupbnd2lem1  27844  nosupbnd2  27845  noinfbnd2lem1  27859  noinfbnd2  27860  eqcuts3  27962  addsproplem3  28129  addsuniflem  28159  negsproplem3  28188  negsunif  28213  mulsproplem10  28283  mulsuniflem  28307  n0cut  28492  n0cut2  28493  n0fincut  28513  zcuts  28565  halfcut  28616  addhalfcut  28617  pw2cut  28618  pw2cutp1  28619  pw2cut2  28620  bdaypw2n0bndlem  28621  bdayfinbndlem1  28625  elreno2  28653  axlowdimlem15  29246  axlowdim  29251  1loopgruspgr  29790  1egrvtxdg1r  29800  1egrvtxdg0  29801  wkslem1  29897  wkslem2  29898  iswlk  29900  redwlk  29960  wlkp1lem8  29968  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  loopclwwlkn1b  30333  clwwlkn1loopb  30334  clwwlknon1  30388  eupth2lem3lem3  30521  frgrncvvdeqlem3  30592  frgrncvvdeqlem5  30594  wlkl0  30658  0ofval  31079  fresunsn  32910  fcnvgreu  32957  cycpm2tr  33379  lindfpropd  33638  nsgqusf1olem1  33665  elrspunidl  33679  opprqusdrng  33719  rprmval  33750  isufd  33774  pidufd  33777  r1pquslmic  33844  selvply1rhmlema  33852  selvply1rhmlemb  33853  selvply1rhmlem1  33854  selvply1rhmlem3  33856  selvply1rhmlem5  33858  selvply1rhm  33859  mplidom  33862  extvfvcl  33870  esplyfval0  33898  esplyfval2  33899  esplyind  33909  vieta  33914  sradrng  33916  rlmdim  33944  ply1degltdimlem  33956  dimkerim  33961  lvecendof1f1o  33967  irngval  34019  extdgfialglem1  34026  minplym1p  34047  minplynzm1p  34048  algextdeglem3  34053  algextdeglem4  34054  algextdeglem5  34055  dispcmp  34193  ordtprsval  34252  ordtprsuni  34253  sitgval  34666  sseqval  34722  reprsuc  34946  lpadval  35010  bnj941  35105  bnj944  35270  revwlk  35515  subfacp1lem5  35574  sconnpht  35619  sconnpht2  35628  sconnpi1  35629  cvmliftlem7  35681  cvmliftlem10  35684  cvmlift2lem13  35705  cvmlift3lem9  35717  satffunlem1lem1  35792  satffunlem2lem1  35794  msrval  35928  mthmpps  35972  onint1  36848  bj-projeq  37515  bj-restsn  37611  finixpnum  38143  matunitlindflem1  38154  ptrest  38157  poimirlem4  38162  poimirlem13  38171  poimirlem14  38172  poimirlem16  38174  poimirlem19  38177  poimirlem26  38184  grpokerinj  38431  isdivrngo  38488  drngoi  38489  isprrngo  38588  lsatset  39653  lsmsat  39671  islshpat  39680  lflsc0N  39746  lkrfval  39750  ldualset  39788  dvafset  41667  dvaset  41668  dvhfset  41743  dvhset  41744  dibffval  41803  dibfval  41804  dib0  41827  cdlemn4a  41862  dihmeetlem4preN  41969  dihmeetlem13N  41982  dih1dimatlem  41992  dihlsprn  41994  dvh2dim  42108  lpolsetN  42145  lclkrlem2j  42179  lclkrlem2p  42185  lcfrlem21  42226  mapdpglem22  42356  mapdpglem23  42357  mapdpglem26  42361  mapdpglem27  42362  mapdpg  42369  baerlem3lem2  42373  baerlem5alem2  42374  baerlem5blem2  42375  baerlem5amN  42379  baerlem5bmN  42380  baerlem5abmN  42381  mapdindp4  42386  mapdhval  42387  mapdheq  42391  mapdh6aN  42398  hvmapffval  42421  hvmapfval  42422  hvmap1o2  42428  hdmap1fval  42459  hdmap1vallem  42460  hdmap1val  42461  hdmap1eq  42464  hdmap1cbv  42465  hdmap1l6a  42472  hdmapfval  42490  hdmap10  42503  hdmaprnlem6N  42517  hgmaprnlem2N  42560  lcmfunnnd  42668  aks6d1c6lem5  42833  qsalrel  42898  frlmsnic  43199  prjspval  43226  prjspval2  43236  prjspnvs  43243  prjcrvfval  43254  dfac11  43680  dfac21  43684  nzprmdif  44920  expgrowth  44936  fzdifsuc2  45920  cnrefiisplem  46434  cnrefiisp  46435  hoidmv1le  47199  ovnovollem3  47263  fsetsniunop  47674  fsetsnf  47676  fsetsnf1  47677  fsetsnfo  47678  dfateq12d  47751  otiunsndisjX  47904  funop1  47908  preimafvelsetpreimafv  48025  imaelsetpreimafv  48032  imasetpreimafvbijlemfo  48042  fundcmpsurbijinjpreimafv  48044  fundcmpsurinj  48046  fundcmpsurbijinj  48047  isprmrng  48989  lmod1zr  49157  0aryfvalel  49298  1arymaptf1  49306  discsubc  49726  imasubclem3  49768  swapf1a  49931  swapf2a  49933  swapf1  49934  swapf2  49936  termcbas2  50144  termchom  50150  termchom2  50151  termcfuncval  50194  mndtcval  50241