Theorem sneqd 4572

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

Syntax hints:   → wi 4   = wceq 1538  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-9 2113  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-sn 4561

This theorem is referenced by:  eqsnuniex  5282  otsndisj  5432  otiunsndisj  5433  iunopeqop  5434  dmsnopss  6120  dmsnsnsn  6126  opswap  6135  ressn  6190  f1osng  6764  fsng  7016  fsn2g  7017  funopsn  7027  funsneqopb  7031  fnressn  7037  2nd1st  7886  dfmpo  7949  cnvf1olem  7957  suppsnop  8001  tpostpos  8069  tfrlem11  8226  ralxpmap  8691  elixpsn  8732  ixpsnf1o  8733  en1b  8820  en1bOLD  8821  mapsnend  8833  xpassen  8860  dif1en  8952  cantnfp1lem3  9445  axdc4lem  10218  ttukeylem3  10274  ttukey2g  10279  fpwwe2lem12  10405  fztp  13319  fzsuc2  13321  fseq1p1m1  13337  fseq1m1p1  13338  expval  13791  hash1elsn  14093  s1val  14310  s1eq  14312  s3sndisj  14685  s3iunsndisj  14686  fsumm1  15470  fprodm1  15684  divalgmod  16122  vdwpc  16688  vdwlem1  16689  vdwlem6  16694  vdwlem7  16695  vdwlem8  16696  cshwsdisj  16807  strle1  16866  setsvalg  16874  setsidvald  16907  setsidvaldOLD  16908  imasval  17229  imasaddvallem  17247  imasvscaval  17256  ismri2dad  17353  mreexd  17358  mreexmrid  17359  homaval  17753  setcmon  17809  funcsetcestrclem1  17878  gsumress  18373  pwsco2mhm  18478  efmnd  18516  idressubmefmnd  18544  smndex1igid  18550  smndex1basss  18551  smndex1mgm  18553  smndex1mndlem  18555  mulgval  18711  idressubgsymg  19025  gsumzaddlem  19529  dmdprd  19608  subgdmdprd  19644  dprdsn  19646  dprd2da  19652  dmdprdpr  19659  dprdpr  19660  dpjfval  19665  dpjval  19666  ablfac1eulem  19682  pgpfaclem1  19691  isunit  19906  isdrng  20002  drngprop  20009  isdrngd  20023  drngpropd  20025  issubdrg  20056  subdrgint  20078  lspsnneg  20275  lspsnsub  20276  lmodindp1  20283  islbs  20345  lspsntrim  20367  lbspropd  20368  lspsnvs  20383  lspsneleq  20384  lspfixed  20397  lpival  20523  zrhrhmb  20719  znval  20746  isobs  20934  frlmval  20962  frlmlbs  21011  islindf  21026  lindfmm  21041  lsslindf  21044  islindf4  21052  islindf5  21053  psrval  21125  mat1dimmul  21632  mat1dimcrng  21633  mat1rhmval  21635  mat1ric  21643  mat1scmat  21695  mdet0pr  21748  m1detdiag  21753  pmatcoe1fsupp  21857  ordtval  22347  ordtcnv  22359  dissnlocfin  22687  ptval2  22759  dfac14  22776  txdis  22790  xkoptsub  22812  pt1hmeo  22964  xpstopnlem1  22967  tgptsmscls  23308  ustuqtoplem  23398  utopsnneiplem  23406  utopsnneip  23407  utop2nei  23409  utop3cls  23410  pcorev2  24198  pcophtb  24199  pi1grplem  24219  pi1inv  24222  cvsunit  24301  i1f1  24861  i1faddlem  24864  i1fmullem  24865  i1fadd  24866  limcfval  25043  dvnfval  25093  ig1pval  25344  0dgrb  25414  dgrnznn  25415  dgreq0  25433  dgrmulc  25439  plyrem  25472  facth  25473  fta1  25475  aaliou2  25507  taylpfval  25531  axlowdimlem15  27331  axlowdim  27336  1loopgruspgr  27874  1egrvtxdg1r  27884  1egrvtxdg0  27885  wkslem1  27981  wkslem2  27982  iswlk  27984  redwlk  28047  wlkp1lem8  28055  crctcshwlkn0lem4  28185  crctcshwlkn0lem5  28186  crctcshwlkn0lem6  28187  loopclwwlkn1b  28413  clwwlkn1loopb  28414  clwwlknon1  28468  eupth2lem3lem3  28601  frgrncvvdeqlem3  28672  frgrncvvdeqlem5  28674  wlkl0  28738  0ofval  29156  fcnvgreu  31017  cycpm2tr  31393  lindfpropd  31583  nsgqusf1olem1  31605  elrspunidl  31613  qsidomlem2  31636  rprmval  31671  sradrng  31680  rgmoddim  31700  dimkerim  31715  dispcmp  31816  ordtprsval  31875  ordtprsuni  31876  indval2  31989  sitgval  32306  sseqval  32362  reprsuc  32602  lpadval  32663  bnj941  32759  bnj944  32925  revwlk  33093  subfacp1lem5  33153  sconnpht  33198  sconnpht2  33207  sconnpi1  33208  cvmliftlem7  33260  cvmliftlem10  33263  cvmlift2lem13  33284  cvmlift3lem9  33296  satffunlem1lem1  33371  satffunlem2lem1  33373  msrval  33507  mthmpps  33551  xpord2pred  33799  xpord3pred  33805  naddcllem  33838  nosupbnd2lem1  33925  nosupbnd2  33926  noinfbnd2lem1  33940  noinfbnd2  33941  onint1  34645  bj-projeq  35189  bj-restsn  35260  finixpnum  35769  matunitlindflem1  35780  ptrest  35783  poimirlem4  35788  poimirlem13  35797  poimirlem14  35798  poimirlem16  35800  poimirlem19  35803  poimirlem26  35810  grpokerinj  36058  isdivrngo  36115  drngoi  36116  isprrngo  36215  lsatset  37009  lsmsat  37027  islshpat  37036  lflsc0N  37102  lkrfval  37106  ldualset  37144  dvafset  39023  dvaset  39024  dvhfset  39099  dvhset  39100  dibffval  39159  dibfval  39160  dib0  39183  cdlemn4a  39218  dihmeetlem4preN  39325  dihmeetlem13N  39338  dih1dimatlem  39348  dihlsprn  39350  dvh2dim  39464  lpolsetN  39501  lclkrlem2j  39535  lclkrlem2p  39541  lcfrlem21  39582  mapdpglem22  39712  mapdpglem23  39713  mapdpglem26  39717  mapdpglem27  39718  mapdpg  39725  baerlem3lem2  39729  baerlem5alem2  39730  baerlem5blem2  39731  baerlem5amN  39735  baerlem5bmN  39736  baerlem5abmN  39737  mapdindp4  39742  mapdhval  39743  mapdheq  39747  mapdh6aN  39754  hvmapffval  39777  hvmapfval  39778  hvmap1o2  39784  hdmap1fval  39815  hdmap1vallem  39816  hdmap1val  39817  hdmap1eq  39820  hdmap1cbv  39821  hdmap1l6a  39828  hdmapfval  39846  hdmap10  39859  hdmaprnlem6N  39873  hgmaprnlem2N  39916  lcmfunnnd  40025  qsalrel  40220  frlmsnic  40268  evlsbagval  40280  prjspval  40447  prjspval2  40457  prjspnvs  40464  prjcrvfval  40473  dfac11  40892  dfac21  40896  nzprmdif  41942  expgrowth  41958  fzdifsuc2  42864  cnrefiisplem  43386  cnrefiisp  43387  hoidmv1le  44149  ovnovollem3  44213  fsetsniunop  44564  fsetsnf  44566  fsetsnf1  44567  fsetsnfo  44568  dfateq12d  44639  otiunsndisjX  44792  funop1  44796  preimafvelsetpreimafv  44861  imaelsetpreimafv  44868  imasetpreimafvbijlemfo  44878  fundcmpsurbijinjpreimafv  44880  fundcmpsurinj  44882  fundcmpsurbijinj  44883  lmod1zr  45855  0aryfvalel  46001  1arymaptf1  46009  mndtcval  46387