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 1537  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-sn 4568

This theorem is referenced by:  otsndisj  5409  otiunsndisj  5410  iunopeqop  5411  dmsnopss  6071  dmsnsnsn  6077  opswap  6086  ressn  6136  f1osng  6655  fsng  6899  fsn2g  6900  funopsn  6910  funsneqopb  6914  fnressn  6920  2nd1st  7737  dfmpo  7797  cnvf1olem  7805  suppsnop  7844  tpostpos  7912  tfrlem11  8024  ralxpmap  8460  elixpsn  8501  ixpsnf1o  8502  en1b  8577  mapsnend  8588  xpassen  8611  cantnfp1lem3  9143  axdc4lem  9877  ttukeylem3  9933  ttukey2g  9938  fpwwe2lem13  10064  fztp  12964  fzsuc2  12966  fseq1p1m1  12982  fseq1m1p1  12983  expval  13432  hash1elsn  13733  s1val  13952  s1eq  13954  s3sndisj  14327  s3iunsndisj  14328  fsumm1  15106  fprodm1  15321  divalgmod  15757  vdwpc  16316  vdwlem1  16317  vdwlem6  16322  vdwlem7  16323  vdwlem8  16324  cshwsdisj  16432  setsvalg  16512  setsidvald  16514  strle1  16592  imasval  16784  imasaddvallem  16802  imasvscaval  16811  ismri2dad  16908  mreexd  16913  mreexmrid  16914  homaval  17291  setcmon  17347  funcsetcestrclem1  17404  gsumress  17892  pwsco2mhm  17997  efmnd  18035  idressubmefmnd  18063  smndex1igid  18069  smndex1basss  18070  smndex1mgm  18072  smndex1mndlem  18074  mulgval  18228  idressubgsymg  18538  gsumzaddlem  19041  dmdprd  19120  subgdmdprd  19156  dprdsn  19158  dprd2da  19164  dmdprdpr  19171  dprdpr  19172  dpjfval  19177  dpjval  19178  ablfac1eulem  19194  pgpfaclem1  19203  isunit  19407  isdrng  19506  drngprop  19513  isdrngd  19527  drngpropd  19529  issubdrg  19560  subdrgint  19582  lspsnneg  19778  lspsnsub  19779  lmodindp1  19786  islbs  19848  lspsntrim  19870  lbspropd  19871  lspsnvs  19886  lspsneleq  19887  lspfixed  19900  lpival  20018  psrval  20142  zrhrhmb  20658  znval  20682  isobs  20864  frlmval  20892  frlmlbs  20941  islindf  20956  lindfmm  20971  lsslindf  20974  islindf4  20982  islindf5  20983  mat1dimmul  21085  mat1dimcrng  21086  mat1rhmval  21088  mat1ric  21096  mat1scmat  21148  mdet0pr  21201  m1detdiag  21206  pmatcoe1fsupp  21309  ordtval  21797  ordtcnv  21809  dissnlocfin  22137  ptval2  22209  dfac14  22226  txdis  22240  xkoptsub  22262  pt1hmeo  22414  xpstopnlem1  22417  tgptsmscls  22758  ustuqtoplem  22848  utopsnneiplem  22856  utopsnneip  22857  utop2nei  22859  utop3cls  22860  pcorev2  23632  pcophtb  23633  pi1grplem  23653  pi1inv  23656  cvsunit  23735  i1f1  24291  i1faddlem  24294  i1fmullem  24295  i1fadd  24296  limcfval  24470  dvnfval  24519  ig1pval  24766  0dgrb  24836  dgrnznn  24837  dgreq0  24855  dgrmulc  24861  plyrem  24894  facth  24895  fta1  24897  aaliou2  24929  taylpfval  24953  axlowdimlem15  26742  axlowdim  26747  1loopgruspgr  27282  1egrvtxdg1r  27292  1egrvtxdg0  27293  wkslem1  27389  wkslem2  27390  iswlk  27392  redwlk  27454  wlkp1lem8  27462  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  loopclwwlkn1b  27820  clwwlkn1loopb  27821  clwwlknon1  27876  eupth2lem3lem3  28009  frgrncvvdeqlem3  28080  frgrncvvdeqlem5  28082  wlkl0  28146  0ofval  28564  fcnvgreu  30418  cycpm2tr  30761  lindfpropd  30942  qsidomlem2  30966  sradrng  30988  rgmoddim  31008  dimkerim  31023  dispcmp  31123  ordtprsval  31161  ordtprsuni  31162  indval2  31273  sitgval  31590  sseqval  31646  reprsuc  31886  lpadval  31947  bnj941  32044  bnj944  32210  revwlk  32371  subfacp1lem5  32431  sconnpht  32476  sconnpht2  32485  sconnpi1  32486  cvmliftlem7  32538  cvmliftlem10  32541  cvmlift2lem13  32562  cvmlift3lem9  32574  satffunlem1lem1  32649  satffunlem2lem1  32651  msrval  32785  mthmpps  32829  nosupbnd2lem1  33215  nosupbnd2  33216  onint1  33797  bj-projeq  34307  bj-restsn  34376  finixpnum  34892  matunitlindflem1  34903  ptrest  34906  poimirlem4  34911  poimirlem13  34920  poimirlem14  34921  poimirlem16  34923  poimirlem19  34926  poimirlem26  34933  grpokerinj  35186  isdivrngo  35243  drngoi  35244  isprrngo  35343  lsatset  36141  lsmsat  36159  islshpat  36168  lflsc0N  36234  lkrfval  36238  ldualset  36276  dvafset  38155  dvaset  38156  dvhfset  38231  dvhset  38232  dibffval  38291  dibfval  38292  dib0  38315  cdlemn4a  38350  dihmeetlem4preN  38457  dihmeetlem13N  38470  dih1dimatlem  38480  dihlsprn  38482  dvh2dim  38596  lpolsetN  38633  lclkrlem2j  38667  lclkrlem2p  38673  lcfrlem21  38714  mapdpglem22  38844  mapdpglem23  38845  mapdpglem26  38849  mapdpglem27  38850  mapdpg  38857  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  baerlem5amN  38867  baerlem5bmN  38868  baerlem5abmN  38869  mapdindp4  38874  mapdhval  38875  mapdheq  38879  mapdh6aN  38886  hvmapffval  38909  hvmapfval  38910  hvmap1o2  38916  hdmap1fval  38947  hdmap1vallem  38948  hdmap1val  38949  hdmap1eq  38952  hdmap1cbv  38953  hdmap1l6a  38960  hdmapfval  38978  hdmap10  38991  hdmaprnlem6N  39005  hgmaprnlem2N  39048  qsalrel  39145  frlmsnic  39169  prjspval  39273  prjspval2  39283  dfac11  39682  dfac21  39686  nzprmdif  40671  expgrowth  40687  fzdifsuc2  41597  cnrefiisplem  42130  cnrefiisp  42131  hoidmv1le  42896  ovnovollem3  42960  dfateq12d  43345  otiunsndisjX  43498  funop1  43502  preimafvelsetpreimafv  43568  imaelsetpreimafv  43575  imasetpreimafvbijlemfo  43585  fundcmpsurbijinjpreimafv  43587  fundcmpsurinj  43589  fundcmpsurbijinj  43590  lmod1zr  44568