Theorem sneqd 4592

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

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

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-sn 4581

This theorem is referenced by:  eqsnuniex  5306  otsndisj  5467  otiunsndisj  5468  iunopeqop  5469  dmsnopss  6172  dmsnsnsn  6178  opswap  6187  ressn  6243  suceqd  6384  f1osng  6816  fsng  7082  fsn2g  7083  funopsn  7093  funsneqopb  7097  fnressn  7103  2nd1st  7982  dfmpo  8044  cnvf1olem  8052  xpord2pred  8087  xpord3pred  8094  suppsnop  8120  tpostpos  8188  tfrlem11  8319  naddcllem  8604  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  en1b  8962  mapsnend  8973  xpassen  8999  dif1en  9086  en1eqsn  9175  cantnfp1lem3  9589  axdc4lem  10365  ttukeylem3  10421  ttukey2g  10426  fpwwe2lem12  10553  fztp  13496  fzsuc2  13498  fseq1p1m1  13514  fseq1m1p1  13515  expval  13986  hash1elsn  14294  s1val  14522  s1eq  14524  s3sndisj  14890  s3iunsndisj  14891  fsumm1  15674  fprodm1  15890  divalgmod  16333  vdwpc  16908  vdwlem1  16909  vdwlem6  16914  vdwlem7  16915  vdwlem8  16916  cshwsdisj  17026  strle1  17085  setsvalg  17093  setsidvald  17126  imasval  17432  imasaddvallem  17450  imasvscaval  17459  ismri2dad  17560  mreexd  17565  mreexmrid  17566  homaval  17955  setcmon  18011  funcsetcestrclem1  18077  chnccats1  18548  chnccat  18549  gsumress  18607  pwsco2mhm  18758  efmnd  18795  idressubmefmnd  18823  smndex1igid  18829  smndex1basss  18830  smndex1mgm  18832  smndex1mndlem  18834  mulgval  19001  idressubgsymg  19339  gsumzaddlem  19850  dmdprd  19929  subgdmdprd  19965  dprdsn  19967  dprd2da  19973  dmdprdpr  19980  dprdpr  19981  dpjfval  19986  dpjval  19987  ablfac1eulem  20003  pgpfaclem1  20012  isunit  20309  isdrng  20666  drngprop  20677  isdrngd  20698  isdrngdOLD  20700  drngpropd  20702  issubdrg  20713  subdrgint  20736  lspsnneg  20957  lspsnsub  20958  lmodindp1  20965  islbs  21028  lspsntrim  21050  lbspropd  21051  lspsnvs  21069  lspsneleq  21070  lspfixed  21083  rngqiprngimf1  21255  lpival  21279  pzriprnglem13  21448  pzriprnglem14  21449  zrhrhmb  21465  znval  21490  isobs  21675  frlmval  21703  frlmlbs  21752  islindf  21767  lindfmm  21782  lsslindf  21785  islindf4  21793  islindf5  21794  psrval  21871  mat1dimmul  22420  mat1dimcrng  22421  mat1rhmval  22423  mat1ric  22431  mat1scmat  22483  mdet0pr  22536  m1detdiag  22541  pmatcoe1fsupp  22645  ordtval  23133  ordtcnv  23145  dissnlocfin  23473  ptval2  23545  dfac14  23562  txdis  23576  xkoptsub  23598  pt1hmeo  23750  xpstopnlem1  23753  tgptsmscls  24094  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  utop2nei  24194  utop3cls  24195  pcorev2  24984  pcophtb  24985  pi1grplem  25005  pi1inv  25008  cvsunit  25087  i1f1  25647  i1faddlem  25650  i1fmullem  25651  i1fadd  25652  limcfval  25829  dvnfval  25880  ig1pval  26137  0dgrb  26207  dgrnznn  26208  dgreq0  26227  dgrmulc  26233  plyrem  26269  facth  26270  fta1  26272  aaliou2  26304  taylpfval  26328  nosupbnd2lem1  27683  nosupbnd2  27684  noinfbnd2lem1  27698  noinfbnd2  27699  eqcuts3  27800  addsproplem3  27967  addsuniflem  27997  negsproplem3  28026  negsunif  28051  mulsproplem10  28121  mulsuniflem  28145  n0cut  28330  n0cut2  28331  n0fincut  28351  zcuts  28403  halfcut  28454  addhalfcut  28455  pw2cut  28456  pw2cutp1  28457  pw2cut2  28458  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  elreno2  28491  axlowdimlem15  29029  axlowdim  29034  1loopgruspgr  29574  1egrvtxdg1r  29584  1egrvtxdg0  29585  wkslem1  29681  wkslem2  29682  iswlk  29684  redwlk  29744  wlkp1lem8  29752  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  loopclwwlkn1b  30117  clwwlkn1loopb  30118  clwwlknon1  30172  eupth2lem3lem3  30305  frgrncvvdeqlem3  30376  frgrncvvdeqlem5  30378  wlkl0  30442  0ofval  30862  fresunsn  32703  fcnvgreu  32751  indval2  32933  cycpm2tr  33201  lindfpropd  33463  nsgqusf1olem1  33494  elrspunidl  33509  qsidomlem2  33534  opprqusdrng  33574  rprmval  33597  isufd  33621  pidufd  33624  r1pquslmic  33692  extvfvcl  33701  esplyfval0  33722  esplyfval2  33723  esplyind  33731  vieta  33736  sradrng  33738  rlmdim  33766  rgmoddimOLD  33767  ply1degltdimlem  33779  dimkerim  33784  lvecendof1f1o  33790  irngval  33842  extdgfialglem1  33849  minplym1p  33870  minplynzm1p  33871  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  dispcmp  34016  ordtprsval  34075  ordtprsuni  34076  sitgval  34489  sseqval  34545  reprsuc  34772  lpadval  34833  bnj941  34928  bnj944  35094  revwlk  35319  subfacp1lem5  35378  sconnpht  35423  sconnpht2  35432  sconnpi1  35433  cvmliftlem7  35485  cvmliftlem10  35488  cvmlift2lem13  35509  cvmlift3lem9  35521  satffunlem1lem1  35596  satffunlem2lem1  35598  msrval  35732  mthmpps  35776  onint1  36643  bj-projeq  37193  bj-restsn  37287  finixpnum  37806  matunitlindflem1  37817  ptrest  37820  poimirlem4  37825  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem19  37840  poimirlem26  37847  grpokerinj  38094  isdivrngo  38151  drngoi  38152  isprrngo  38251  lsatset  39250  lsmsat  39268  islshpat  39277  lflsc0N  39343  lkrfval  39347  ldualset  39385  dvafset  41264  dvaset  41265  dvhfset  41340  dvhset  41341  dibffval  41400  dibfval  41401  dib0  41424  cdlemn4a  41459  dihmeetlem4preN  41566  dihmeetlem13N  41579  dih1dimatlem  41589  dihlsprn  41591  dvh2dim  41705  lpolsetN  41742  lclkrlem2j  41776  lclkrlem2p  41782  lcfrlem21  41823  mapdpglem22  41953  mapdpglem23  41954  mapdpglem26  41958  mapdpglem27  41959  mapdpg  41966  baerlem3lem2  41970  baerlem5alem2  41971  baerlem5blem2  41972  baerlem5amN  41976  baerlem5bmN  41977  baerlem5abmN  41978  mapdindp4  41983  mapdhval  41984  mapdheq  41988  mapdh6aN  41995  hvmapffval  42018  hvmapfval  42019  hvmap1o2  42025  hdmap1fval  42056  hdmap1vallem  42057  hdmap1val  42058  hdmap1eq  42061  hdmap1cbv  42062  hdmap1l6a  42069  hdmapfval  42087  hdmap10  42100  hdmaprnlem6N  42114  hgmaprnlem2N  42157  lcmfunnnd  42266  aks6d1c6lem5  42431  qsalrel  42496  frlmsnic  42795  prjspval  42846  prjspval2  42856  prjspnvs  42863  prjcrvfval  42874  dfac11  43304  dfac21  43308  nzprmdif  44560  expgrowth  44576  fzdifsuc2  45558  cnrefiisplem  46073  cnrefiisp  46074  hoidmv1le  46838  ovnovollem3  46902  fsetsniunop  47295  fsetsnf  47297  fsetsnf1  47298  fsetsnfo  47299  dfateq12d  47372  otiunsndisjX  47525  funop1  47529  preimafvelsetpreimafv  47634  imaelsetpreimafv  47641  imasetpreimafvbijlemfo  47651  fundcmpsurbijinjpreimafv  47653  fundcmpsurinj  47655  fundcmpsurbijinj  47656  lmod1zr  48739  0aryfvalel  48880  1arymaptf1  48888  discsubc  49309  imasubclem3  49351  swapf1a  49514  swapf2a  49516  swapf1  49517  swapf2  49519  termcbas2  49727  termchom  49733  termchom2  49734  termcfuncval  49777  mndtcval  49824