Theorem sneqd 4639

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

Syntax hints:   → wi 4   = wceq 1541  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-sn 4628

This theorem is referenced by:  eqsnuniex  5358  otsndisj  5518  otiunsndisj  5519  iunopeqop  5520  dmsnopss  6210  dmsnsnsn  6216  opswap  6225  ressn  6281  f1osng  6871  fsng  7131  fsn2g  7132  funopsn  7142  funsneqopb  7146  fnressn  7152  2nd1st  8020  dfmpo  8084  cnvf1olem  8092  xpord2pred  8127  xpord3pred  8134  suppsnop  8159  tpostpos  8227  tfrlem11  8384  naddcllem  8671  ralxpmap  8886  elixpsn  8927  ixpsnf1o  8928  en1b  9019  en1bOLD  9020  mapsnend  9032  xpassen  9062  dif1en  9156  dif1enOLD  9158  en1eqsn  9270  cantnfp1lem3  9671  axdc4lem  10446  ttukeylem3  10502  ttukey2g  10507  fpwwe2lem12  10633  fztp  13553  fzsuc2  13555  fseq1p1m1  13571  fseq1m1p1  13572  expval  14025  hash1elsn  14327  s1val  14544  s1eq  14546  s3sndisj  14910  s3iunsndisj  14911  fsumm1  15693  fprodm1  15907  divalgmod  16345  vdwpc  16909  vdwlem1  16910  vdwlem6  16915  vdwlem7  16916  vdwlem8  16917  cshwsdisj  17028  strle1  17087  setsvalg  17095  setsidvald  17128  setsidvaldOLD  17129  imasval  17453  imasaddvallem  17471  imasvscaval  17480  ismri2dad  17577  mreexd  17582  mreexmrid  17583  homaval  17977  setcmon  18033  funcsetcestrclem1  18102  gsumress  18597  pwsco2mhm  18710  efmnd  18747  idressubmefmnd  18775  smndex1igid  18781  smndex1basss  18782  smndex1mgm  18784  smndex1mndlem  18786  mulgval  18948  idressubgsymg  19272  gsumzaddlem  19783  dmdprd  19862  subgdmdprd  19898  dprdsn  19900  dprd2da  19906  dmdprdpr  19913  dprdpr  19914  dpjfval  19919  dpjval  19920  ablfac1eulem  19936  pgpfaclem1  19945  isunit  20179  isdrng  20311  drngprop  20322  isdrngd  20340  isdrngdOLD  20342  drngpropd  20344  issubdrg  20381  subdrgint  20411  lspsnneg  20609  lspsnsub  20610  lmodindp1  20617  islbs  20679  lspsntrim  20701  lbspropd  20702  lspsnvs  20719  lspsneleq  20720  lspfixed  20733  lpival  20875  zrhrhmb  21051  znval  21078  isobs  21266  frlmval  21294  frlmlbs  21343  islindf  21358  lindfmm  21373  lsslindf  21376  islindf4  21384  islindf5  21385  psrval  21459  mat1dimmul  21969  mat1dimcrng  21970  mat1rhmval  21972  mat1ric  21980  mat1scmat  22032  mdet0pr  22085  m1detdiag  22090  pmatcoe1fsupp  22194  ordtval  22684  ordtcnv  22696  dissnlocfin  23024  ptval2  23096  dfac14  23113  txdis  23127  xkoptsub  23149  pt1hmeo  23301  xpstopnlem1  23304  tgptsmscls  23645  ustuqtoplem  23735  utopsnneiplem  23743  utopsnneip  23744  utop2nei  23746  utop3cls  23747  pcorev2  24535  pcophtb  24536  pi1grplem  24556  pi1inv  24559  cvsunit  24638  i1f1  25198  i1faddlem  25201  i1fmullem  25202  i1fadd  25203  limcfval  25380  dvnfval  25430  ig1pval  25681  0dgrb  25751  dgrnznn  25752  dgreq0  25770  dgrmulc  25776  plyrem  25809  facth  25810  fta1  25812  aaliou2  25844  taylpfval  25868  nosupbnd2lem1  27207  nosupbnd2  27208  noinfbnd2lem1  27222  noinfbnd2  27223  addsproplem3  27444  addsuniflem  27473  negsproplem3  27493  negsunif  27518  mulsproplem10  27570  mulsuniflem  27593  axlowdimlem15  28203  axlowdim  28208  1loopgruspgr  28746  1egrvtxdg1r  28756  1egrvtxdg0  28757  wkslem1  28853  wkslem2  28854  iswlk  28856  redwlk  28918  wlkp1lem8  28926  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem6  29058  loopclwwlkn1b  29284  clwwlkn1loopb  29285  clwwlknon1  29339  eupth2lem3lem3  29472  frgrncvvdeqlem3  29543  frgrncvvdeqlem5  29545  wlkl0  29609  0ofval  30027  fcnvgreu  31885  cycpm2tr  32265  lindfpropd  32486  nsgqusf1olem1  32512  elrspunidl  32534  qsidomlem2  32560  opprqusdrng  32595  rprmval  32621  sradrng  32661  rlmdim  32682  rgmoddimOLD  32683  ply1degltdimlem  32695  dimkerim  32700  irngval  32737  algextdeglem1  32760  dispcmp  32827  ordtprsval  32886  ordtprsuni  32887  indval2  33000  sitgval  33319  sseqval  33375  reprsuc  33615  lpadval  33676  bnj941  33771  bnj944  33937  revwlk  34103  subfacp1lem5  34163  sconnpht  34208  sconnpht2  34217  sconnpi1  34218  cvmliftlem7  34270  cvmliftlem10  34273  cvmlift2lem13  34294  cvmlift3lem9  34306  satffunlem1lem1  34381  satffunlem2lem1  34383  msrval  34517  mthmpps  34561  onint1  35322  bj-projeq  35861  bj-restsn  35951  finixpnum  36461  matunitlindflem1  36472  ptrest  36475  poimirlem4  36480  poimirlem13  36489  poimirlem14  36490  poimirlem16  36492  poimirlem19  36495  poimirlem26  36502  grpokerinj  36749  isdivrngo  36806  drngoi  36807  isprrngo  36906  lsatset  37848  lsmsat  37866  islshpat  37875  lflsc0N  37941  lkrfval  37945  ldualset  37983  dvafset  39863  dvaset  39864  dvhfset  39939  dvhset  39940  dibffval  39999  dibfval  40000  dib0  40023  cdlemn4a  40058  dihmeetlem4preN  40165  dihmeetlem13N  40178  dih1dimatlem  40188  dihlsprn  40190  dvh2dim  40304  lpolsetN  40341  lclkrlem2j  40375  lclkrlem2p  40381  lcfrlem21  40422  mapdpglem22  40552  mapdpglem23  40553  mapdpglem26  40557  mapdpglem27  40558  mapdpg  40565  baerlem3lem2  40569  baerlem5alem2  40570  baerlem5blem2  40571  baerlem5amN  40575  baerlem5bmN  40576  baerlem5abmN  40577  mapdindp4  40582  mapdhval  40583  mapdheq  40587  mapdh6aN  40594  hvmapffval  40617  hvmapfval  40618  hvmap1o2  40624  hdmap1fval  40655  hdmap1vallem  40656  hdmap1val  40657  hdmap1eq  40660  hdmap1cbv  40661  hdmap1l6a  40668  hdmapfval  40686  hdmap10  40699  hdmaprnlem6N  40713  hgmaprnlem2N  40756  lcmfunnnd  40865  qsalrel  41059  frlmsnic  41107  prjspval  41341  prjspval2  41351  prjspnvs  41358  prjcrvfval  41369  dfac11  41789  dfac21  41793  nzprmdif  43063  expgrowth  43079  fzdifsuc2  44006  cnrefiisplem  44531  cnrefiisp  44532  hoidmv1le  45296  ovnovollem3  45360  fsetsniunop  45745  fsetsnf  45747  fsetsnf1  45748  fsetsnfo  45749  dfateq12d  45820  otiunsndisjX  45973  funop1  45977  preimafvelsetpreimafv  46042  imaelsetpreimafv  46049  imasetpreimafvbijlemfo  46059  fundcmpsurbijinjpreimafv  46061  fundcmpsurinj  46063  fundcmpsurbijinj  46064  rngqiprngimf1  46765  lmod1zr  47127  0aryfvalel  47273  1arymaptf1  47281  mndtcval  47658