Theorem sneqd 4618

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-sn 4607

This theorem is referenced by:  eqsnuniex  5336  otsndisj  5499  otiunsndisj  5500  iunopeqop  5501  dmsnopss  6208  dmsnsnsn  6214  opswap  6223  ressn  6279  f1osng  6864  fsng  7132  fsn2g  7133  funopsn  7143  funsneqopb  7147  fnressn  7153  2nd1st  8042  dfmpo  8106  cnvf1olem  8114  xpord2pred  8149  xpord3pred  8156  suppsnop  8182  tpostpos  8250  tfrlem11  8407  naddcllem  8693  ralxpmap  8915  elixpsn  8956  ixpsnf1o  8957  en1b  9044  mapsnend  9055  xpassen  9085  dif1en  9179  dif1enOLD  9181  en1eqsn  9285  cantnfp1lem3  9699  axdc4lem  10474  ttukeylem3  10530  ttukey2g  10535  fpwwe2lem12  10661  fztp  13602  fzsuc2  13604  fseq1p1m1  13620  fseq1m1p1  13621  expval  14086  hash1elsn  14394  s1val  14621  s1eq  14623  s3sndisj  14991  s3iunsndisj  14992  fsumm1  15772  fprodm1  15988  divalgmod  16430  vdwpc  17005  vdwlem1  17006  vdwlem6  17011  vdwlem7  17012  vdwlem8  17013  cshwsdisj  17123  strle1  17182  setsvalg  17190  setsidvald  17223  imasval  17530  imasaddvallem  17548  imasvscaval  17557  ismri2dad  17654  mreexd  17659  mreexmrid  17660  homaval  18049  setcmon  18105  funcsetcestrclem1  18171  gsumress  18665  pwsco2mhm  18816  efmnd  18853  idressubmefmnd  18881  smndex1igid  18887  smndex1basss  18888  smndex1mgm  18890  smndex1mndlem  18892  mulgval  19059  idressubgsymg  19396  gsumzaddlem  19907  dmdprd  19986  subgdmdprd  20022  dprdsn  20024  dprd2da  20030  dmdprdpr  20037  dprdpr  20038  dpjfval  20043  dpjval  20044  ablfac1eulem  20060  pgpfaclem1  20069  isunit  20338  isdrng  20698  drngprop  20709  isdrngd  20730  isdrngdOLD  20732  drngpropd  20734  issubdrg  20745  subdrgint  20768  lspsnneg  20968  lspsnsub  20969  lmodindp1  20976  islbs  21039  lspsntrim  21061  lbspropd  21062  lspsnvs  21080  lspsneleq  21081  lspfixed  21094  rngqiprngimf1  21266  lpival  21290  pzriprnglem13  21459  pzriprnglem14  21460  zrhrhmb  21476  znval  21501  isobs  21685  frlmval  21713  frlmlbs  21762  islindf  21777  lindfmm  21792  lsslindf  21795  islindf4  21803  islindf5  21804  psrval  21880  mat1dimmul  22419  mat1dimcrng  22420  mat1rhmval  22422  mat1ric  22430  mat1scmat  22482  mdet0pr  22535  m1detdiag  22540  pmatcoe1fsupp  22644  ordtval  23132  ordtcnv  23144  dissnlocfin  23472  ptval2  23544  dfac14  23561  txdis  23575  xkoptsub  23597  pt1hmeo  23749  xpstopnlem1  23752  tgptsmscls  24093  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  utop2nei  24194  utop3cls  24195  pcorev2  24984  pcophtb  24985  pi1grplem  25005  pi1inv  25008  cvsunit  25087  i1f1  25648  i1faddlem  25651  i1fmullem  25652  i1fadd  25653  limcfval  25830  dvnfval  25881  ig1pval  26138  0dgrb  26208  dgrnznn  26209  dgreq0  26228  dgrmulc  26234  plyrem  26270  facth  26271  fta1  26273  aaliou2  26305  taylpfval  26329  nosupbnd2lem1  27684  nosupbnd2  27685  noinfbnd2lem1  27699  noinfbnd2  27700  addsproplem3  27935  addsuniflem  27965  negsproplem3  27993  negsunif  28018  mulsproplem10  28085  mulsuniflem  28109  n0scut  28283  n0scut2  28284  n0sfincut  28303  zscut  28352  halfcut  28390  addhalfcut  28391  pw2cut  28392  pw2cutp1  28393  zs12bday  28400  axlowdimlem15  28940  axlowdim  28945  1loopgruspgr  29485  1egrvtxdg1r  29495  1egrvtxdg0  29496  wkslem1  29592  wkslem2  29593  iswlk  29595  redwlk  29657  wlkp1lem8  29665  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  loopclwwlkn1b  30028  clwwlkn1loopb  30029  clwwlknon1  30083  eupth2lem3lem3  30216  frgrncvvdeqlem3  30287  frgrncvvdeqlem5  30289  wlkl0  30353  0ofval  30773  fcnvgreu  32656  indval2  32836  chnccats1  33000  cycpm2tr  33135  lindfpropd  33402  nsgqusf1olem1  33433  elrspunidl  33448  qsidomlem2  33473  opprqusdrng  33513  rprmval  33536  isufd  33560  pidufd  33563  r1pquslmic  33625  sradrng  33627  rlmdim  33654  rgmoddimOLD  33655  ply1degltdimlem  33667  dimkerim  33672  lvecendof1f1o  33678  irngval  33731  minplym1p  33752  minplynzm1p  33753  algextdeglem3  33758  algextdeglem4  33759  algextdeglem5  33760  dispcmp  33895  ordtprsval  33954  ordtprsuni  33955  sitgval  34369  sseqval  34425  reprsuc  34652  lpadval  34713  bnj941  34808  bnj944  34974  revwlk  35152  subfacp1lem5  35211  sconnpht  35256  sconnpht2  35265  sconnpi1  35266  cvmliftlem7  35318  cvmliftlem10  35321  cvmlift2lem13  35342  cvmlift3lem9  35354  satffunlem1lem1  35429  satffunlem2lem1  35431  msrval  35565  mthmpps  35609  onint1  36472  bj-projeq  37015  bj-restsn  37105  finixpnum  37634  matunitlindflem1  37645  ptrest  37648  poimirlem4  37653  poimirlem13  37662  poimirlem14  37663  poimirlem16  37665  poimirlem19  37668  poimirlem26  37675  grpokerinj  37922  isdivrngo  37979  drngoi  37980  isprrngo  38079  lsatset  39013  lsmsat  39031  islshpat  39040  lflsc0N  39106  lkrfval  39110  ldualset  39148  dvafset  41028  dvaset  41029  dvhfset  41104  dvhset  41105  dibffval  41164  dibfval  41165  dib0  41188  cdlemn4a  41223  dihmeetlem4preN  41330  dihmeetlem13N  41343  dih1dimatlem  41353  dihlsprn  41355  dvh2dim  41469  lpolsetN  41506  lclkrlem2j  41540  lclkrlem2p  41546  lcfrlem21  41587  mapdpglem22  41717  mapdpglem23  41718  mapdpglem26  41722  mapdpglem27  41723  mapdpg  41730  baerlem3lem2  41734  baerlem5alem2  41735  baerlem5blem2  41736  baerlem5amN  41740  baerlem5bmN  41741  baerlem5abmN  41742  mapdindp4  41747  mapdhval  41748  mapdheq  41752  mapdh6aN  41759  hvmapffval  41782  hvmapfval  41783  hvmap1o2  41789  hdmap1fval  41820  hdmap1vallem  41821  hdmap1val  41822  hdmap1eq  41825  hdmap1cbv  41826  hdmap1l6a  41833  hdmapfval  41851  hdmap10  41864  hdmaprnlem6N  41878  hgmaprnlem2N  41921  lcmfunnnd  42030  aks6d1c6lem5  42195  qsalrel  42258  frlmsnic  42538  prjspval  42601  prjspval2  42611  prjspnvs  42618  prjcrvfval  42629  dfac11  43061  dfac21  43065  nzprmdif  44318  expgrowth  44334  fzdifsuc2  45319  cnrefiisplem  45838  cnrefiisp  45839  hoidmv1le  46603  ovnovollem3  46667  fsetsniunop  47058  fsetsnf  47060  fsetsnf1  47061  fsetsnfo  47062  dfateq12d  47135  otiunsndisjX  47288  funop1  47292  preimafvelsetpreimafv  47382  imaelsetpreimafv  47389  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  fundcmpsurinj  47403  fundcmpsurbijinj  47404  lmod1zr  48449  0aryfvalel  48594  1arymaptf1  48602  discsubc  49011  imasubclem3  49045  swapf1a  49166  swapf2a  49168  swapf1  49169  swapf2  49171  termcbas2  49347  termchom  49353  termchom2  49354  termcfuncval  49397  mndtcval  49436