Theorem sneqd 4642

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

Syntax hints:   → wi 4   = wceq 1536  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-sn 4631

This theorem is referenced by:  eqsnuniex  5366  otsndisj  5528  otiunsndisj  5529  iunopeqop  5530  dmsnopss  6235  dmsnsnsn  6241  opswap  6250  ressn  6306  f1osng  6889  fsng  7156  fsn2g  7157  funopsn  7167  funsneqopb  7171  fnressn  7177  2nd1st  8061  dfmpo  8125  cnvf1olem  8133  xpord2pred  8168  xpord3pred  8175  suppsnop  8201  tpostpos  8269  tfrlem11  8426  naddcllem  8712  ralxpmap  8934  elixpsn  8975  ixpsnf1o  8976  en1b  9063  mapsnend  9074  xpassen  9104  dif1en  9198  dif1enOLD  9200  en1eqsn  9305  cantnfp1lem3  9717  axdc4lem  10492  ttukeylem3  10548  ttukey2g  10553  fpwwe2lem12  10679  fztp  13616  fzsuc2  13618  fseq1p1m1  13634  fseq1m1p1  13635  expval  14100  hash1elsn  14406  s1val  14632  s1eq  14634  s3sndisj  15002  s3iunsndisj  15003  fsumm1  15783  fprodm1  15999  divalgmod  16439  vdwpc  17013  vdwlem1  17014  vdwlem6  17019  vdwlem7  17020  vdwlem8  17021  cshwsdisj  17132  strle1  17191  setsvalg  17199  setsidvald  17232  setsidvaldOLD  17233  imasval  17557  imasaddvallem  17575  imasvscaval  17584  ismri2dad  17681  mreexd  17686  mreexmrid  17687  homaval  18084  setcmon  18140  funcsetcestrclem1  18209  gsumress  18707  pwsco2mhm  18858  efmnd  18895  idressubmefmnd  18923  smndex1igid  18929  smndex1basss  18930  smndex1mgm  18932  smndex1mndlem  18934  mulgval  19101  idressubgsymg  19442  gsumzaddlem  19953  dmdprd  20032  subgdmdprd  20068  dprdsn  20070  dprd2da  20076  dmdprdpr  20083  dprdpr  20084  dpjfval  20089  dpjval  20090  ablfac1eulem  20106  pgpfaclem1  20115  isunit  20389  isdrng  20749  drngprop  20760  isdrngd  20781  isdrngdOLD  20783  drngpropd  20785  issubdrg  20797  subdrgint  20820  lspsnneg  21021  lspsnsub  21022  lmodindp1  21029  islbs  21092  lspsntrim  21114  lbspropd  21115  lspsnvs  21133  lspsneleq  21134  lspfixed  21147  rngqiprngimf1  21327  lpival  21351  pzriprnglem13  21521  pzriprnglem14  21522  zrhrhmb  21538  znval  21567  isobs  21757  frlmval  21785  frlmlbs  21834  islindf  21849  lindfmm  21864  lsslindf  21867  islindf4  21875  islindf5  21876  psrval  21952  mat1dimmul  22497  mat1dimcrng  22498  mat1rhmval  22500  mat1ric  22508  mat1scmat  22560  mdet0pr  22613  m1detdiag  22618  pmatcoe1fsupp  22722  ordtval  23212  ordtcnv  23224  dissnlocfin  23552  ptval2  23624  dfac14  23641  txdis  23655  xkoptsub  23677  pt1hmeo  23829  xpstopnlem1  23832  tgptsmscls  24173  ustuqtoplem  24263  utopsnneiplem  24271  utopsnneip  24272  utop2nei  24274  utop3cls  24275  pcorev2  25074  pcophtb  25075  pi1grplem  25095  pi1inv  25098  cvsunit  25177  i1f1  25738  i1faddlem  25741  i1fmullem  25742  i1fadd  25743  limcfval  25921  dvnfval  25972  ig1pval  26229  0dgrb  26299  dgrnznn  26300  dgreq0  26319  dgrmulc  26325  plyrem  26361  facth  26362  fta1  26364  aaliou2  26396  taylpfval  26420  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbnd2lem1  27789  noinfbnd2  27790  addsproplem3  28018  addsuniflem  28048  negsproplem3  28076  negsunif  28101  mulsproplem10  28165  mulsuniflem  28189  n0scut  28352  n0sbday  28368  zscut  28407  halfcut  28430  cutpw2  28431  addhalfcut  28433  pw2cut  28434  zs12bday  28438  axlowdimlem15  28985  axlowdim  28990  1loopgruspgr  29532  1egrvtxdg1r  29542  1egrvtxdg0  29543  wkslem1  29639  wkslem2  29640  iswlk  29642  redwlk  29704  wlkp1lem8  29712  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  loopclwwlkn1b  30070  clwwlkn1loopb  30071  clwwlknon1  30125  eupth2lem3lem3  30258  frgrncvvdeqlem3  30329  frgrncvvdeqlem5  30331  wlkl0  30395  0ofval  30815  fcnvgreu  32689  cycpm2tr  33121  lindfpropd  33389  nsgqusf1olem1  33420  elrspunidl  33435  qsidomlem2  33460  opprqusdrng  33500  rprmval  33523  isufd  33547  pidufd  33550  r1pquslmic  33610  sradrng  33612  rlmdim  33636  rgmoddimOLD  33637  ply1degltdimlem  33649  dimkerim  33654  lvecendof1f1o  33660  irngval  33699  minplym1p  33720  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  dispcmp  33819  ordtprsval  33878  ordtprsuni  33879  indval2  33994  sitgval  34313  sseqval  34369  reprsuc  34608  lpadval  34669  bnj941  34764  bnj944  34930  revwlk  35108  subfacp1lem5  35168  sconnpht  35213  sconnpht2  35222  sconnpi1  35223  cvmliftlem7  35275  cvmliftlem10  35278  cvmlift2lem13  35299  cvmlift3lem9  35311  satffunlem1lem1  35386  satffunlem2lem1  35388  msrval  35522  mthmpps  35566  onint1  36431  bj-projeq  36974  bj-restsn  37064  finixpnum  37591  matunitlindflem1  37602  ptrest  37605  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  poimirlem26  37632  grpokerinj  37879  isdivrngo  37936  drngoi  37937  isprrngo  38036  lsatset  38971  lsmsat  38989  islshpat  38998  lflsc0N  39064  lkrfval  39068  ldualset  39106  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  dibffval  41122  dibfval  41123  dib0  41146  cdlemn4a  41181  dihmeetlem4preN  41288  dihmeetlem13N  41301  dih1dimatlem  41311  dihlsprn  41313  dvh2dim  41427  lpolsetN  41464  lclkrlem2j  41498  lclkrlem2p  41504  lcfrlem21  41545  mapdpglem22  41675  mapdpglem23  41676  mapdpglem26  41680  mapdpglem27  41681  mapdpg  41688  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdindp4  41705  mapdhval  41706  mapdheq  41710  mapdh6aN  41717  hvmapffval  41740  hvmapfval  41741  hvmap1o2  41747  hdmap1fval  41778  hdmap1vallem  41779  hdmap1val  41780  hdmap1eq  41783  hdmap1cbv  41784  hdmap1l6a  41791  hdmapfval  41809  hdmap10  41822  hdmaprnlem6N  41836  hgmaprnlem2N  41879  lcmfunnnd  41993  aks6d1c6lem5  42158  qsalrel  42259  frlmsnic  42526  prjspval  42589  prjspval2  42599  prjspnvs  42606  prjcrvfval  42617  dfac11  43050  dfac21  43054  nzprmdif  44314  expgrowth  44330  fzdifsuc2  45260  cnrefiisplem  45784  cnrefiisp  45785  hoidmv1le  46549  ovnovollem3  46613  fsetsniunop  46998  fsetsnf  47000  fsetsnf1  47001  fsetsnfo  47002  dfateq12d  47075  otiunsndisjX  47228  funop1  47232  preimafvelsetpreimafv  47312  imaelsetpreimafv  47319  imasetpreimafvbijlemfo  47329  fundcmpsurbijinjpreimafv  47331  fundcmpsurinj  47333  fundcmpsurbijinj  47334  lmod1zr  48338  0aryfvalel  48483  1arymaptf1  48491  mndtcval  48887