Theorem sneqd 4597

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

Syntax hints:   → wi 4   = wceq 1540  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4586

This theorem is referenced by:  eqsnuniex  5311  otsndisj  5474  otiunsndisj  5475  iunopeqop  5476  dmsnopss  6175  dmsnsnsn  6181  opswap  6190  ressn  6246  suceqd  6387  f1osng  6823  fsng  7091  fsn2g  7092  funopsn  7102  funsneqopb  7106  fnressn  7112  2nd1st  7996  dfmpo  8058  cnvf1olem  8066  xpord2pred  8101  xpord3pred  8108  suppsnop  8134  tpostpos  8202  tfrlem11  8333  naddcllem  8617  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  en1b  8973  mapsnend  8984  xpassen  9012  dif1en  9101  dif1enOLD  9103  en1eqsn  9195  cantnfp1lem3  9609  axdc4lem  10384  ttukeylem3  10440  ttukey2g  10445  fpwwe2lem12  10571  fztp  13517  fzsuc2  13519  fseq1p1m1  13535  fseq1m1p1  13536  expval  14004  hash1elsn  14312  s1val  14539  s1eq  14541  s3sndisj  14909  s3iunsndisj  14910  fsumm1  15693  fprodm1  15909  divalgmod  16352  vdwpc  16927  vdwlem1  16928  vdwlem6  16933  vdwlem7  16934  vdwlem8  16935  cshwsdisj  17045  strle1  17104  setsvalg  17112  setsidvald  17145  imasval  17450  imasaddvallem  17468  imasvscaval  17477  ismri2dad  17574  mreexd  17579  mreexmrid  17580  homaval  17969  setcmon  18025  funcsetcestrclem1  18091  gsumress  18585  pwsco2mhm  18736  efmnd  18773  idressubmefmnd  18801  smndex1igid  18807  smndex1basss  18808  smndex1mgm  18810  smndex1mndlem  18812  mulgval  18979  idressubgsymg  19316  gsumzaddlem  19827  dmdprd  19906  subgdmdprd  19942  dprdsn  19944  dprd2da  19950  dmdprdpr  19957  dprdpr  19958  dpjfval  19963  dpjval  19964  ablfac1eulem  19980  pgpfaclem1  19989  isunit  20258  isdrng  20618  drngprop  20629  isdrngd  20650  isdrngdOLD  20652  drngpropd  20654  issubdrg  20665  subdrgint  20688  lspsnneg  20888  lspsnsub  20889  lmodindp1  20896  islbs  20959  lspsntrim  20981  lbspropd  20982  lspsnvs  21000  lspsneleq  21001  lspfixed  21014  rngqiprngimf1  21186  lpival  21210  pzriprnglem13  21379  pzriprnglem14  21380  zrhrhmb  21396  znval  21421  isobs  21605  frlmval  21633  frlmlbs  21682  islindf  21697  lindfmm  21712  lsslindf  21715  islindf4  21723  islindf5  21724  psrval  21800  mat1dimmul  22339  mat1dimcrng  22340  mat1rhmval  22342  mat1ric  22350  mat1scmat  22402  mdet0pr  22455  m1detdiag  22460  pmatcoe1fsupp  22564  ordtval  23052  ordtcnv  23064  dissnlocfin  23392  ptval2  23464  dfac14  23481  txdis  23495  xkoptsub  23517  pt1hmeo  23669  xpstopnlem1  23672  tgptsmscls  24013  ustuqtoplem  24103  utopsnneiplem  24111  utopsnneip  24112  utop2nei  24114  utop3cls  24115  pcorev2  24904  pcophtb  24905  pi1grplem  24925  pi1inv  24928  cvsunit  25007  i1f1  25567  i1faddlem  25570  i1fmullem  25571  i1fadd  25572  limcfval  25749  dvnfval  25800  ig1pval  26057  0dgrb  26127  dgrnznn  26128  dgreq0  26147  dgrmulc  26153  plyrem  26189  facth  26190  fta1  26192  aaliou2  26224  taylpfval  26248  nosupbnd2lem1  27603  nosupbnd2  27604  noinfbnd2lem1  27618  noinfbnd2  27619  addsproplem3  27854  addsuniflem  27884  negsproplem3  27912  negsunif  27937  mulsproplem10  28004  mulsuniflem  28028  n0scut  28202  n0scut2  28203  n0sfincut  28222  zscut  28271  halfcut  28309  addhalfcut  28310  pw2cut  28311  pw2cutp1  28312  zs12bday  28319  axlowdimlem15  28859  axlowdim  28864  1loopgruspgr  29404  1egrvtxdg1r  29414  1egrvtxdg0  29415  wkslem1  29511  wkslem2  29512  iswlk  29514  redwlk  29574  wlkp1lem8  29582  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  crctcshwlkn0lem6  29718  loopclwwlkn1b  29944  clwwlkn1loopb  29945  clwwlknon1  29999  eupth2lem3lem3  30132  frgrncvvdeqlem3  30203  frgrncvvdeqlem5  30205  wlkl0  30269  0ofval  30689  fcnvgreu  32570  indval2  32750  chnccats1  32914  cycpm2tr  33049  lindfpropd  33326  nsgqusf1olem1  33357  elrspunidl  33372  qsidomlem2  33397  opprqusdrng  33437  rprmval  33460  isufd  33484  pidufd  33487  r1pquslmic  33549  sradrng  33551  rlmdim  33578  rgmoddimOLD  33579  ply1degltdimlem  33591  dimkerim  33596  lvecendof1f1o  33602  irngval  33653  minplym1p  33676  minplynzm1p  33677  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  dispcmp  33822  ordtprsval  33881  ordtprsuni  33882  sitgval  34296  sseqval  34352  reprsuc  34579  lpadval  34640  bnj941  34735  bnj944  34901  revwlk  35085  subfacp1lem5  35144  sconnpht  35189  sconnpht2  35198  sconnpi1  35199  cvmliftlem7  35251  cvmliftlem10  35254  cvmlift2lem13  35275  cvmlift3lem9  35287  satffunlem1lem1  35362  satffunlem2lem1  35364  msrval  35498  mthmpps  35542  onint1  36410  bj-projeq  36953  bj-restsn  37043  finixpnum  37572  matunitlindflem1  37583  ptrest  37586  poimirlem4  37591  poimirlem13  37600  poimirlem14  37601  poimirlem16  37603  poimirlem19  37606  poimirlem26  37613  grpokerinj  37860  isdivrngo  37917  drngoi  37918  isprrngo  38017  lsatset  38956  lsmsat  38974  islshpat  38983  lflsc0N  39049  lkrfval  39053  ldualset  39091  dvafset  40971  dvaset  40972  dvhfset  41047  dvhset  41048  dibffval  41107  dibfval  41108  dib0  41131  cdlemn4a  41166  dihmeetlem4preN  41273  dihmeetlem13N  41286  dih1dimatlem  41296  dihlsprn  41298  dvh2dim  41412  lpolsetN  41449  lclkrlem2j  41483  lclkrlem2p  41489  lcfrlem21  41530  mapdpglem22  41660  mapdpglem23  41661  mapdpglem26  41665  mapdpglem27  41666  mapdpg  41673  baerlem3lem2  41677  baerlem5alem2  41678  baerlem5blem2  41679  baerlem5amN  41683  baerlem5bmN  41684  baerlem5abmN  41685  mapdindp4  41690  mapdhval  41691  mapdheq  41695  mapdh6aN  41702  hvmapffval  41725  hvmapfval  41726  hvmap1o2  41732  hdmap1fval  41763  hdmap1vallem  41764  hdmap1val  41765  hdmap1eq  41768  hdmap1cbv  41769  hdmap1l6a  41776  hdmapfval  41794  hdmap10  41807  hdmaprnlem6N  41821  hgmaprnlem2N  41864  lcmfunnnd  41973  aks6d1c6lem5  42138  qsalrel  42201  frlmsnic  42501  prjspval  42564  prjspval2  42574  prjspnvs  42581  prjcrvfval  42592  dfac11  43024  dfac21  43028  nzprmdif  44281  expgrowth  44297  fzdifsuc2  45281  cnrefiisplem  45800  cnrefiisp  45801  hoidmv1le  46565  ovnovollem3  46629  fsetsniunop  47023  fsetsnf  47025  fsetsnf1  47026  fsetsnfo  47027  dfateq12d  47100  otiunsndisjX  47253  funop1  47257  preimafvelsetpreimafv  47362  imaelsetpreimafv  47369  imasetpreimafvbijlemfo  47379  fundcmpsurbijinjpreimafv  47381  fundcmpsurinj  47383  fundcmpsurbijinj  47384  lmod1zr  48455  0aryfvalel  48596  1arymaptf1  48604  discsubc  49026  imasubclem3  49068  swapf1a  49231  swapf2a  49233  swapf1  49234  swapf2  49236  termcbas2  49444  termchom  49450  termchom2  49451  termcfuncval  49494  mndtcval  49541