Theorem sneqd 4601

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

Syntax hints:   → wi 4   = wceq 1570  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-sn 4590

This theorem is referenced by:  eqsnuniex  5332  otsndisj  5502  otiunsndisj  5503  iunopeqop  5504  iunopeqopOLD  5505  dmsnopss  6215  dmsnsnsn  6221  opswap  6230  ressn  6286  suceqd  6428  f1osng  6863  fsng  7133  fsn2g  7134  funopsn  7144  funopsnOLD  7145  funsneqopb  7149  fnressn  7155  2nd1st  8031  dfmpo  8093  cnvf1olem  8101  xpord2pred  8137  xpord3pred  8144  suppsnop  8170  tpostpos  8238  tfrlem11  8371  naddcllem  8658  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  en1b  9018  mapsnend  9029  xpassen  9055  dif1en  9142  en1eqsn  9231  cantnfp1lem3  9645  axdc4lem  10434  ttukeylem3  10490  ttukey2g  10495  fpwwe2lem12  10622  indval2  12218  fztp  13604  fzsuc2  13606  fseq1p1m1  13622  fseq1m1p1  13623  expval  14095  hash1elsn  14403  s1val  14632  s1eq  14634  s3sndisj  15000  s3iunsndisj  15001  fsumm1  15798  fprodm1  16017  divalgmod  16459  vdwpc  17035  vdwlem1  17036  vdwlem6  17041  vdwlem7  17042  vdwlem8  17043  cshwsdisj  17153  strle1  17213  setsvalg  17221  setsidvald  17254  imasval  17560  imasaddvallem  17578  imasvscaval  17587  ismri2dad  17688  mreexd  17693  mreexmrid  17694  homaval  18083  setcmon  18139  funcsetcestrclem1  18205  chnccats1  18676  chnccat  18677  gsumress  18735  pwsco2mhm  18887  efmnd  18924  idressubmefmnd  18952  smndex1igid  18960  smndex1igidOLD  18961  smndex1basss  18962  smndex1mgm  18964  smndex1mndlem  18966  mulgval  19132  idressubgsymg  19475  gsumzaddlem  19986  dmdprd  20065  subgdmdprd  20101  dprdsn  20103  dprd2da  20109  dmdprdpr  20116  dprdpr  20117  dpjfval  20122  dpjval  20123  ablfac1eulem  20139  pgpfaclem1  20148  isunit  20451  isdrng  20831  drngprop  20844  isdrngd  20868  isdrngdOLD  20870  drngpropd  20873  issubdrg  20883  subdrgint  20906  lspsnneg  21127  lspsnsub  21128  lmodindp1  21135  islbs  21197  lspsntrim  21219  lbspropd  21220  lspsnvs  21238  lspsneleq  21239  lspfixed  21252  rngqiprngimf1  21440  qsidomlem2  21481  lpival  21492  pzriprnglem13  21643  pzriprnglem14  21644  zrhrhmb  21660  znval  21685  isobs  21870  frlmval  21898  frlmlbs  21947  islindf  21962  lindfmm  21977  lsslindf  21980  islindf4  21988  islindf5  21989  psrval  22065  mat1dimmul  22633  mat1dimcrng  22634  mat1rhmval  22636  mat1ric  22644  mat1scmat  22696  mdet0pr  22749  m1detdiag  22754  pmatcoe1fsupp  22858  ordtval  23346  ordtcnv  23358  dissnlocfin  23686  ptval2  23758  dfac14  23775  txdis  23789  xkoptsub  23811  pt1hmeo  23963  xpstopnlem1  23966  tgptsmscls  24307  ustuqtoplem  24396  utopsnneiplem  24404  utopsnneip  24405  utop2nei  24407  utop3cls  24408  pcorev2  25187  pcophtb  25188  pi1grplem  25208  pi1inv  25211  cvsunit  25290  i1f1  25849  i1faddlem  25852  i1fmullem  25853  i1fadd  25854  limcfval  26031  dvnfval  26081  ig1pval  26333  0dgrb  26403  dgrnznn  26404  dgreq0  26422  dgrmulc  26428  plyrem  26466  facth  26467  fta1  26469  aaliou2  26503  taylpfval  26528  nosupbnd2lem1  27879  nosupbnd2  27880  noinfbnd2lem1  27894  noinfbnd2  27895  eqcuts3  27997  addsproplem3  28164  addsuniflem  28194  negsproplem3  28223  negsunif  28248  mulsproplem10  28318  mulsuniflem  28342  n0cut  28527  n0cut2  28528  n0fincut  28548  zcuts  28600  halfcut  28651  addhalfcut  28652  pw2cut  28653  pw2cutp1  28654  pw2cut2  28655  bdaypw2n0bndlem  28656  bdayfinbndlem1  28660  elreno2  28688  axlowdimlem15  29306  axlowdim  29311  1loopgruspgr  29850  1egrvtxdg1r  29860  1egrvtxdg0  29861  wkslem1  29957  wkslem2  29958  iswlk  29960  redwlk  30020  wlkp1lem8  30028  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  loopclwwlkn1b  30393  clwwlkn1loopb  30394  clwwlknon1  30448  eupth2lem3lem3  30581  frgrncvvdeqlem3  30652  frgrncvvdeqlem5  30654  wlkl0  30718  0ofval  31139  fresunsn  32970  fcnvgreu  33017  cycpm2tr  33439  lindfpropd  33695  nsgqusf1olem1  33722  elrspunidl  33736  opprqusdrng  33775  rprmval  33806  isufd  33830  pidufd  33833  r1pquslmic  33900  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem3  33912  selvply1rhmlem5  33914  selvply1rhm  33915  mplidom  33918  extvfvcl  33926  esplyfval0  33954  esplyfval2  33955  esplyind  33965  vieta  33970  sradrng  33972  rlmdim  34000  ply1degltdimlem  34012  dimkerim  34017  lvecendof1f1o  34023  irngval  34075  extdgfialglem1  34082  minplym1p  34103  minplynzm1p  34104  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  dispcmp  34249  ordtprsval  34308  ordtprsuni  34309  sitgval  34722  sseqval  34778  reprsuc  35002  lpadval  35066  bnj941  35161  bnj944  35326  revwlk  35617  subfacp1lem5  35676  sconnpht  35721  sconnpht2  35730  sconnpi1  35731  cvmliftlem7  35783  cvmliftlem10  35786  cvmlift2lem13  35807  cvmlift3lem9  35819  satffunlem1lem1  35894  satffunlem2lem1  35896  msrval  36030  mthmpps  36074  onint1  36960  bj-projeq  37628  bj-restsn  37724  finixpnum  38256  matunitlindflem1  38267  ptrest  38270  poimirlem4  38275  poimirlem13  38284  poimirlem14  38285  poimirlem16  38287  poimirlem19  38290  poimirlem26  38297  grpokerinj  38544  isdivrngo  38601  drngoi  38602  isprrngo  38701  lsatset  39764  lsmsat  39782  islshpat  39791  lflsc0N  39857  lkrfval  39861  ldualset  39899  dvafset  41778  dvaset  41779  dvhfset  41854  dvhset  41855  dibffval  41914  dibfval  41915  dib0  41938  cdlemn4a  41973  dihmeetlem4preN  42080  dihmeetlem13N  42093  dih1dimatlem  42103  dihlsprn  42105  dvh2dim  42219  lpolsetN  42256  lclkrlem2j  42290  lclkrlem2p  42296  lcfrlem21  42337  mapdpglem22  42467  mapdpglem23  42468  mapdpglem26  42472  mapdpglem27  42473  mapdpg  42480  baerlem3lem2  42484  baerlem5alem2  42485  baerlem5blem2  42486  baerlem5amN  42490  baerlem5bmN  42491  baerlem5abmN  42492  mapdindp4  42497  mapdhval  42498  mapdheq  42502  mapdh6aN  42509  hvmapffval  42532  hvmapfval  42533  hvmap1o2  42539  hdmap1fval  42570  hdmap1vallem  42571  hdmap1val  42572  hdmap1eq  42575  hdmap1cbv  42576  hdmap1l6a  42583  hdmapfval  42601  hdmap10  42614  hdmaprnlem6N  42628  hgmaprnlem2N  42671  lcmfunnnd  42779  aks6d1c6lem5  42944  qsalrel  43009  frlmsnic  43308  prjspval  43335  prjspval2  43345  prjspnvs  43352  prjcrvfval  43363  dfac11  43789  dfac21  43793  nzprmdif  45029  expgrowth  45045  fzdifsuc2  46029  cnrefiisplem  46543  cnrefiisp  46544  hoidmv1le  47308  ovnovollem3  47372  fsetsniunop  47786  fsetsnf  47788  fsetsnf1  47789  fsetsnfo  47790  dfateq12d  47863  otiunsndisjX  48016  funop1  48020  preimafvelsetpreimafv  48137  imaelsetpreimafv  48144  imasetpreimafvbijlemfo  48154  fundcmpsurbijinjpreimafv  48156  fundcmpsurinj  48158  fundcmpsurbijinj  48159  isprmrng  49101  lmod1zr  49273  0aryfvalel  49414  1arymaptf1  49422  discsubc  49842  imasubclem3  49884  swapf1a  50047  swapf2a  50049  swapf1  50050  swapf2  50052  termcbas2  50260  termchom  50266  termchom2  50267  termcfuncval  50310  mndtcval  50357