Theorem sneqd 4641

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-sn 4630

This theorem is referenced by:  eqsnuniex  5360  otsndisj  5520  otiunsndisj  5521  iunopeqop  5522  dmsnopss  6214  dmsnsnsn  6220  opswap  6229  ressn  6285  f1osng  6875  fsng  7135  fsn2g  7136  funopsn  7146  funsneqopb  7150  fnressn  7156  2nd1st  8024  dfmpo  8088  cnvf1olem  8096  xpord2pred  8131  xpord3pred  8138  suppsnop  8163  tpostpos  8231  tfrlem11  8388  naddcllem  8675  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  en1b  9023  en1bOLD  9024  mapsnend  9036  xpassen  9066  dif1en  9160  dif1enOLD  9162  en1eqsn  9274  cantnfp1lem3  9675  axdc4lem  10450  ttukeylem3  10506  ttukey2g  10511  fpwwe2lem12  10637  fztp  13557  fzsuc2  13559  fseq1p1m1  13575  fseq1m1p1  13576  expval  14029  hash1elsn  14331  s1val  14548  s1eq  14550  s3sndisj  14914  s3iunsndisj  14915  fsumm1  15697  fprodm1  15911  divalgmod  16349  vdwpc  16913  vdwlem1  16914  vdwlem6  16919  vdwlem7  16920  vdwlem8  16921  cshwsdisj  17032  strle1  17091  setsvalg  17099  setsidvald  17132  setsidvaldOLD  17133  imasval  17457  imasaddvallem  17475  imasvscaval  17484  ismri2dad  17581  mreexd  17586  mreexmrid  17587  homaval  17981  setcmon  18037  funcsetcestrclem1  18106  gsumress  18601  pwsco2mhm  18714  efmnd  18751  idressubmefmnd  18779  smndex1igid  18785  smndex1basss  18786  smndex1mgm  18788  smndex1mndlem  18790  mulgval  18954  idressubgsymg  19278  gsumzaddlem  19789  dmdprd  19868  subgdmdprd  19904  dprdsn  19906  dprd2da  19912  dmdprdpr  19919  dprdpr  19920  dpjfval  19925  dpjval  19926  ablfac1eulem  19942  pgpfaclem1  19951  isunit  20187  isdrng  20361  drngprop  20372  isdrngd  20390  isdrngdOLD  20392  drngpropd  20394  issubdrg  20401  subdrgint  20419  lspsnneg  20617  lspsnsub  20618  lmodindp1  20625  islbs  20687  lspsntrim  20709  lbspropd  20710  lspsnvs  20727  lspsneleq  20728  lspfixed  20741  lpival  20883  zrhrhmb  21060  znval  21087  isobs  21275  frlmval  21303  frlmlbs  21352  islindf  21367  lindfmm  21382  lsslindf  21385  islindf4  21393  islindf5  21394  psrval  21468  mat1dimmul  21978  mat1dimcrng  21979  mat1rhmval  21981  mat1ric  21989  mat1scmat  22041  mdet0pr  22094  m1detdiag  22099  pmatcoe1fsupp  22203  ordtval  22693  ordtcnv  22705  dissnlocfin  23033  ptval2  23105  dfac14  23122  txdis  23136  xkoptsub  23158  pt1hmeo  23310  xpstopnlem1  23313  tgptsmscls  23654  ustuqtoplem  23744  utopsnneiplem  23752  utopsnneip  23753  utop2nei  23755  utop3cls  23756  pcorev2  24544  pcophtb  24545  pi1grplem  24565  pi1inv  24568  cvsunit  24647  i1f1  25207  i1faddlem  25210  i1fmullem  25211  i1fadd  25212  limcfval  25389  dvnfval  25439  ig1pval  25690  0dgrb  25760  dgrnznn  25761  dgreq0  25779  dgrmulc  25785  plyrem  25818  facth  25819  fta1  25821  aaliou2  25853  taylpfval  25877  nosupbnd2lem1  27218  nosupbnd2  27219  noinfbnd2lem1  27233  noinfbnd2  27234  addsproplem3  27455  addsuniflem  27484  negsproplem3  27504  negsunif  27529  mulsproplem10  27581  mulsuniflem  27604  axlowdimlem15  28214  axlowdim  28219  1loopgruspgr  28757  1egrvtxdg1r  28767  1egrvtxdg0  28768  wkslem1  28864  wkslem2  28865  iswlk  28867  redwlk  28929  wlkp1lem8  28937  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem6  29069  loopclwwlkn1b  29295  clwwlkn1loopb  29296  clwwlknon1  29350  eupth2lem3lem3  29483  frgrncvvdeqlem3  29554  frgrncvvdeqlem5  29556  wlkl0  29620  0ofval  30040  fcnvgreu  31898  cycpm2tr  32278  lindfpropd  32498  nsgqusf1olem1  32524  elrspunidl  32546  qsidomlem2  32572  opprqusdrng  32607  rprmval  32633  sradrng  32673  rlmdim  32694  rgmoddimOLD  32695  ply1degltdimlem  32707  dimkerim  32712  irngval  32749  algextdeglem1  32772  dispcmp  32839  ordtprsval  32898  ordtprsuni  32899  indval2  33012  sitgval  33331  sseqval  33387  reprsuc  33627  lpadval  33688  bnj941  33783  bnj944  33949  revwlk  34115  subfacp1lem5  34175  sconnpht  34220  sconnpht2  34229  sconnpi1  34230  cvmliftlem7  34282  cvmliftlem10  34285  cvmlift2lem13  34306  cvmlift3lem9  34318  satffunlem1lem1  34393  satffunlem2lem1  34395  msrval  34529  mthmpps  34573  onint1  35334  bj-projeq  35873  bj-restsn  35963  finixpnum  36473  matunitlindflem1  36484  ptrest  36487  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem16  36504  poimirlem19  36507  poimirlem26  36514  grpokerinj  36761  isdivrngo  36818  drngoi  36819  isprrngo  36918  lsatset  37860  lsmsat  37878  islshpat  37887  lflsc0N  37953  lkrfval  37957  ldualset  37995  dvafset  39875  dvaset  39876  dvhfset  39951  dvhset  39952  dibffval  40011  dibfval  40012  dib0  40035  cdlemn4a  40070  dihmeetlem4preN  40177  dihmeetlem13N  40190  dih1dimatlem  40200  dihlsprn  40202  dvh2dim  40316  lpolsetN  40353  lclkrlem2j  40387  lclkrlem2p  40393  lcfrlem21  40434  mapdpglem22  40564  mapdpglem23  40565  mapdpglem26  40569  mapdpglem27  40570  mapdpg  40577  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  baerlem5amN  40587  baerlem5bmN  40588  baerlem5abmN  40589  mapdindp4  40594  mapdhval  40595  mapdheq  40599  mapdh6aN  40606  hvmapffval  40629  hvmapfval  40630  hvmap1o2  40636  hdmap1fval  40667  hdmap1vallem  40668  hdmap1val  40669  hdmap1eq  40672  hdmap1cbv  40673  hdmap1l6a  40680  hdmapfval  40698  hdmap10  40711  hdmaprnlem6N  40725  hgmaprnlem2N  40768  lcmfunnnd  40877  qsalrel  41062  frlmsnic  41110  prjspval  41345  prjspval2  41355  prjspnvs  41362  prjcrvfval  41373  dfac11  41804  dfac21  41808  nzprmdif  43078  expgrowth  43094  fzdifsuc2  44020  cnrefiisplem  44545  cnrefiisp  44546  hoidmv1le  45310  ovnovollem3  45374  fsetsniunop  45759  fsetsnf  45761  fsetsnf1  45762  fsetsnfo  45763  dfateq12d  45834  otiunsndisjX  45987  funop1  45991  preimafvelsetpreimafv  46056  imaelsetpreimafv  46063  imasetpreimafvbijlemfo  46073  fundcmpsurbijinjpreimafv  46075  fundcmpsurinj  46077  fundcmpsurbijinj  46078  rngqiprngimf1  46785  pzriprnglem13  46817  pzriprnglem14  46818  lmod1zr  47174  0aryfvalel  47320  1arymaptf1  47328  mndtcval  47705