Theorem sneqd 4570

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

Syntax hints:   → wi 4   = wceq 1539  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-sn 4559

This theorem is referenced by:  eqsnuniex  5278  otsndisj  5427  otiunsndisj  5428  iunopeqop  5429  dmsnopss  6106  dmsnsnsn  6112  opswap  6121  ressn  6177  f1osng  6740  fsng  6991  fsn2g  6992  funopsn  7002  funsneqopb  7006  fnressn  7012  2nd1st  7852  dfmpo  7913  cnvf1olem  7921  suppsnop  7965  tpostpos  8033  tfrlem11  8190  ralxpmap  8642  elixpsn  8683  ixpsnf1o  8684  en1b  8767  en1bOLD  8768  mapsnend  8780  xpassen  8806  dif1en  8907  cantnfp1lem3  9368  axdc4lem  10142  ttukeylem3  10198  ttukey2g  10203  fpwwe2lem12  10329  fztp  13241  fzsuc2  13243  fseq1p1m1  13259  fseq1m1p1  13260  expval  13712  hash1elsn  14014  s1val  14231  s1eq  14233  s3sndisj  14606  s3iunsndisj  14607  fsumm1  15391  fprodm1  15605  divalgmod  16043  vdwpc  16609  vdwlem1  16610  vdwlem6  16615  vdwlem7  16616  vdwlem8  16617  cshwsdisj  16728  strle1  16787  setsvalg  16795  setsidvald  16828  setsidvaldOLD  16829  imasval  17139  imasaddvallem  17157  imasvscaval  17166  ismri2dad  17263  mreexd  17268  mreexmrid  17269  homaval  17662  setcmon  17718  funcsetcestrclem1  17787  gsumress  18281  pwsco2mhm  18386  efmnd  18424  idressubmefmnd  18452  smndex1igid  18458  smndex1basss  18459  smndex1mgm  18461  smndex1mndlem  18463  mulgval  18619  idressubgsymg  18933  gsumzaddlem  19437  dmdprd  19516  subgdmdprd  19552  dprdsn  19554  dprd2da  19560  dmdprdpr  19567  dprdpr  19568  dpjfval  19573  dpjval  19574  ablfac1eulem  19590  pgpfaclem1  19599  isunit  19814  isdrng  19910  drngprop  19917  isdrngd  19931  drngpropd  19933  issubdrg  19964  subdrgint  19986  lspsnneg  20183  lspsnsub  20184  lmodindp1  20191  islbs  20253  lspsntrim  20275  lbspropd  20276  lspsnvs  20291  lspsneleq  20292  lspfixed  20305  lpival  20429  zrhrhmb  20624  znval  20651  isobs  20837  frlmval  20865  frlmlbs  20914  islindf  20929  lindfmm  20944  lsslindf  20947  islindf4  20955  islindf5  20956  psrval  21028  mat1dimmul  21533  mat1dimcrng  21534  mat1rhmval  21536  mat1ric  21544  mat1scmat  21596  mdet0pr  21649  m1detdiag  21654  pmatcoe1fsupp  21758  ordtval  22248  ordtcnv  22260  dissnlocfin  22588  ptval2  22660  dfac14  22677  txdis  22691  xkoptsub  22713  pt1hmeo  22865  xpstopnlem1  22868  tgptsmscls  23209  ustuqtoplem  23299  utopsnneiplem  23307  utopsnneip  23308  utop2nei  23310  utop3cls  23311  pcorev2  24097  pcophtb  24098  pi1grplem  24118  pi1inv  24121  cvsunit  24200  i1f1  24759  i1faddlem  24762  i1fmullem  24763  i1fadd  24764  limcfval  24941  dvnfval  24991  ig1pval  25242  0dgrb  25312  dgrnznn  25313  dgreq0  25331  dgrmulc  25337  plyrem  25370  facth  25371  fta1  25373  aaliou2  25405  taylpfval  25429  axlowdimlem15  27227  axlowdim  27232  1loopgruspgr  27770  1egrvtxdg1r  27780  1egrvtxdg0  27781  wkslem1  27877  wkslem2  27878  iswlk  27880  redwlk  27942  wlkp1lem8  27950  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  loopclwwlkn1b  28307  clwwlkn1loopb  28308  clwwlknon1  28362  eupth2lem3lem3  28495  frgrncvvdeqlem3  28566  frgrncvvdeqlem5  28568  wlkl0  28632  0ofval  29050  fcnvgreu  30912  cycpm2tr  31288  lindfpropd  31478  nsgqusf1olem1  31500  elrspunidl  31508  qsidomlem2  31531  rprmval  31566  sradrng  31575  rgmoddim  31595  dimkerim  31610  dispcmp  31711  ordtprsval  31770  ordtprsuni  31771  indval2  31882  sitgval  32199  sseqval  32255  reprsuc  32495  lpadval  32556  bnj941  32652  bnj944  32818  revwlk  32986  subfacp1lem5  33046  sconnpht  33091  sconnpht2  33100  sconnpi1  33101  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift2lem13  33177  cvmlift3lem9  33189  satffunlem1lem1  33264  satffunlem2lem1  33266  msrval  33400  mthmpps  33444  xpord2pred  33719  xpord3pred  33725  naddcllem  33758  nosupbnd2lem1  33845  nosupbnd2  33846  noinfbnd2lem1  33860  noinfbnd2  33861  onint1  34565  bj-projeq  35109  bj-restsn  35180  finixpnum  35689  matunitlindflem1  35700  ptrest  35703  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem16  35720  poimirlem19  35723  poimirlem26  35730  grpokerinj  35978  isdivrngo  36035  drngoi  36036  isprrngo  36135  lsatset  36931  lsmsat  36949  islshpat  36958  lflsc0N  37024  lkrfval  37028  ldualset  37066  dvafset  38945  dvaset  38946  dvhfset  39021  dvhset  39022  dibffval  39081  dibfval  39082  dib0  39105  cdlemn4a  39140  dihmeetlem4preN  39247  dihmeetlem13N  39260  dih1dimatlem  39270  dihlsprn  39272  dvh2dim  39386  lpolsetN  39423  lclkrlem2j  39457  lclkrlem2p  39463  lcfrlem21  39504  mapdpglem22  39634  mapdpglem23  39635  mapdpglem26  39639  mapdpglem27  39640  mapdpg  39647  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdindp4  39664  mapdhval  39665  mapdheq  39669  mapdh6aN  39676  hvmapffval  39699  hvmapfval  39700  hvmap1o2  39706  hdmap1fval  39737  hdmap1vallem  39738  hdmap1val  39739  hdmap1eq  39742  hdmap1cbv  39743  hdmap1l6a  39750  hdmapfval  39768  hdmap10  39781  hdmaprnlem6N  39795  hgmaprnlem2N  39838  lcmfunnnd  39948  qsalrel  40141  frlmsnic  40188  evlsbagval  40198  prjspval  40363  prjspval2  40373  prjspnvs  40380  dfac11  40803  dfac21  40807  nzprmdif  41826  expgrowth  41842  fzdifsuc2  42739  cnrefiisplem  43260  cnrefiisp  43261  hoidmv1le  44022  ovnovollem3  44086  fsetsniunop  44430  fsetsnf  44432  fsetsnf1  44433  fsetsnfo  44434  dfateq12d  44505  otiunsndisjX  44658  funop1  44662  preimafvelsetpreimafv  44728  imaelsetpreimafv  44735  imasetpreimafvbijlemfo  44745  fundcmpsurbijinjpreimafv  44747  fundcmpsurinj  44749  fundcmpsurbijinj  44750  lmod1zr  45722  0aryfvalel  45868  1arymaptf1  45876  mndtcval  46252