Theorem sneqd 4603

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-sn 4592

This theorem is used by:  eqsnuniex  5334  otsndisj  5504  otiunsndisj  5505  iunopeqop  5506  iunopeqopOLD  5507  dmsnopss  6217  dmsnsnsn  6223  opswap  6232  ressn  6290  suceqd  6432  f1osng  6867  fsng  7137  fsn2g  7138  funopsn  7150  funopsnOLD  7151  funsneqopb  7155  fnressn  7161  2nd1st  8041  dfmpo  8103  cnvf1olem  8111  xpord2pred  8147  xpord3pred  8154  suppsnop  8180  tpostpos  8248  tfrlem11  8381  naddcllem  8668  ralxpmap  8900  elixpsn  8941  ixpsnf1o  8942  en1b  9028  mapsnend  9040  xpassen  9066  dif1en  9153  en1eqsn  9242  cantnfp1lem3  9656  axdc4lem  10454  ttukeylem3  10510  ttukey2g  10515  fpwwe2lem12  10642  indval2  12238  fztp  13625  fzsuc2  13627  fseq1p1m1  13643  fseq1m1p1  13644  expval  14117  hash1elsn  14425  s1val  14655  s1eq  14657  s3sndisj  15028  s3iunsndisj  15029  fsumm1  15825  fprodm1  16044  divalgmod  16486  vdwpc  17062  vdwlem1  17063  vdwlem6  17068  vdwlem7  17069  vdwlem8  17070  cshwsdisj  17180  strle1  17240  setsvalg  17248  setsidvald  17281  imasval  17587  imasaddvallem  17605  imasvscaval  17614  ismri2dad  17715  mreexd  17720  mreexmrid  17721  homaval  18110  setcmon  18166  funcsetcestrclem1  18232  chnccats1  18703  chnccat  18704  gsumress  18772  pwsco2mhm  18929  efmnd  18966  idressubmefmnd  18994  smndex1igid  19002  smndex1igidOLD  19003  smndex1basss  19004  smndex1mgm  19006  smndex1mndlem  19008  mulgval  19181  idressubgsymg  19524  gsumzaddlem  20035  dmdprd  20114  subgdmdprd  20150  dprdsn  20152  dprd2da  20158  dmdprdpr  20165  dprdpr  20166  dpjfval  20171  dpjval  20172  ablfac1eulem  20188  pgpfaclem1  20197  isunit  20501  isdrng  20881  drngprop  20894  isdrngd  20918  isdrngdOLD  20920  drngpropd  20923  issubdrg  20933  subdrgint  20956  lspsnneg  21177  lspsnsub  21178  lmodindp1  21185  islbs  21247  lspsntrim  21269  lbspropd  21270  lspsnvs  21288  lspsneleq  21289  lspfixed  21302  rngqiprngimf1  21490  qsidomlem2  21531  lpival  21542  pzriprnglem13  21693  pzriprnglem14  21694  zrhrhmb  21710  znval  21735  isobs  21920  frlmval  21948  frlmlbs  21997  islindf  22012  lindfmm  22027  lsslindf  22030  islindf4  22038  islindf5  22039  psrval  22115  mat1dimmul  22683  mat1dimcrng  22684  mat1rhmval  22686  mat1ric  22694  mat1scmat  22746  mdet0pr  22799  m1detdiag  22804  pmatcoe1fsupp  22908  ordtval  23396  ordtcnv  23408  dissnlocfin  23737  ptval2  23809  dfac14  23826  txdis  23840  xkoptsub  23862  pt1hmeo  24014  xpstopnlem1  24017  tgptsmscls  24358  ustuqtoplem  24447  utopsnneiplem  24455  utopsnneip  24456  utop2nei  24458  utop3cls  24459  pcorev2  25238  pcophtb  25239  pi1grplem  25259  pi1inv  25262  cvsunit  25341  i1f1  25900  i1faddlem  25903  i1fmullem  25904  i1fadd  25905  limcfval  26082  dvnfval  26132  ig1pval  26384  0dgrb  26454  dgrnznn  26455  dgreq0  26473  dgrmulc  26479  plyrem  26517  facth  26518  fta1  26520  aaliou2  26554  taylpfval  26579  nosupbnd2lem1  27930  nosupbnd2  27931  noinfbnd2lem1  27945  noinfbnd2  27946  eqcuts3  28048  addsproplem3  28215  addsuniflem  28245  negsproplem3  28274  negsunif  28299  mulsproplem10  28369  mulsuniflem  28393  n0cut  28578  n0cut2  28579  n0fincut  28599  zcuts  28651  halfcut  28702  addhalfcut  28703  pw2cut  28704  pw2cutp1  28705  pw2cut2  28706  bdaypw2n0bndlem  28707  bdayfinbndlem1  28711  elreno2  28739  axlowdimlem15  29361  axlowdim  29366  1loopgruspgr  29908  1egrvtxdg1r  29918  1egrvtxdg0  29919  wkslem1  30015  wkslem2  30016  iswlk  30018  redwlk  30078  wlkp1lem8  30086  revwlk  30094  crctcshwlkn0lem4  30229  crctcshwlkn0lem5  30230  crctcshwlkn0lem6  30231  loopclwwlkn1b  30460  clwwlkn1loopb  30461  clwwlknon1  30515  eupth2lem3lem3  30652  frgrncvvdeqlem3  30723  frgrncvvdeqlem5  30725  wlkl0  30789  0ofval  31210  fresunsn  33041  fcnvgreu  33088  cycpm2tr  33503  lindfpropd  33759  nsgqusf1olem1  33786  elrspunidl  33800  opprqusdrng  33839  rprmval  33870  isufd  33894  pidufd  33897  r1pquslmic  33964  selvply1rhmlema  33972  selvply1rhmlemb  33973  selvply1rhmlem1  33974  selvply1rhmlem3  33976  selvply1rhmlem5  33978  selvply1rhm  33979  mplidom  33982  extvfvcl  33990  esplyfval0  34018  esplyfval2  34019  esplyind  34029  vieta  34034  sradrng  34036  rlmdim  34064  ply1degltdimlem  34076  dimkerim  34081  lvecendof1f1o  34087  irngval  34139  extdgfialglem1  34146  minplym1p  34167  minplynzm1p  34168  algextdeglem3  34173  algextdeglem4  34174  algextdeglem5  34175  dispcmp  34313  ordtprsval  34372  ordtprsuni  34373  sitgval  34787  sseqval  34843  reprsuc  35067  lpadval  35131  bnj941  35226  bnj944  35391  subfacp1lem5  35713  sconnpht  35758  sconnpht2  35767  sconnpi1  35768  cvmliftlem7  35820  cvmliftlem10  35823  cvmlift2lem13  35844  cvmlift3lem9  35856  satffunlem1lem1  35931  satffunlem2lem1  35933  msrval  36067  mthmpps  36111  onint1  37017  bj-projeq  37685  bj-restsn  37781  finixpnum  38313  matunitlindflem1  38324  ptrest  38327  poimirlem4  38332  poimirlem13  38341  poimirlem14  38342  poimirlem16  38344  poimirlem19  38347  poimirlem26  38354  grpokerinj  38602  isdivrngo  38659  drngoi  38660  isprrngo  38759  lsatset  39822  lsmsat  39840  islshpat  39849  lflsc0N  39915  lkrfval  39919  ldualset  39957  dvafset  41836  dvaset  41837  dvhfset  41912  dvhset  41913  dibffval  41972  dibfval  41973  dib0  41996  cdlemn4a  42031  dihmeetlem4preN  42138  dihmeetlem13N  42151  dih1dimatlem  42161  dihlsprn  42163  dvh2dim  42277  lpolsetN  42314  lclkrlem2j  42348  lclkrlem2p  42354  lcfrlem21  42395  mapdpglem22  42525  mapdpglem23  42526  mapdpglem26  42530  mapdpglem27  42531  mapdpg  42538  baerlem3lem2  42542  baerlem5alem2  42543  baerlem5blem2  42544  baerlem5amN  42548  baerlem5bmN  42549  baerlem5abmN  42550  mapdindp4  42555  mapdhval  42556  mapdheq  42560  mapdh6aN  42567  hvmapffval  42590  hvmapfval  42591  hvmap1o2  42597  hdmap1fval  42628  hdmap1vallem  42629  hdmap1val  42630  hdmap1eq  42633  hdmap1cbv  42634  hdmap1l6a  42641  hdmapfval  42659  hdmap10  42672  hdmaprnlem6N  42686  hgmaprnlem2N  42729  lcmfunnnd  42837  aks6d1c6lem5  43002  qsalrel  43067  frlmsnic  43366  prjspval  43393  prjspval2  43403  prjspnvs  43410  prjcrvfval  43421  dfac11  43847  dfac21  43851  nzprmdif  45087  expgrowth  45103  fzdifsuc2  46087  cnrefiisplem  46601  cnrefiisp  46602  hoidmv1le  47366  ovnovollem3  47430  fsetsniunop  47844  fsetsnf  47846  fsetsnf1  47847  fsetsnfo  47848  dfateq12d  47921  otiunsndisjX  48074  funop1  48078  preimafvelsetpreimafv  48195  imaelsetpreimafv  48202  imasetpreimafvbijlemfo  48212  fundcmpsurbijinjpreimafv  48214  fundcmpsurinj  48216  fundcmpsurbijinj  48217  isprmrng  49158  lmod1zr  49330  0aryfvalel  49471  1arymaptf1  49479  discsubc  49899  imasubclem3  49941  swapf1a  50104  swapf2a  50106  swapf1  50107  swapf2  50109  termcbas2  50317  termchom  50323  termchom2  50324  termcfuncval  50367  mndtcval  50414