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 17	1 ⊢ (𝜑 → {𝐴} = {𝐵})

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-sn 4592

This theorem is referenced by:  eqsnuniex  5321  otsndisj  5481  otiunsndisj  5482  iunopeqop  5483  dmsnopss  6171  dmsnsnsn  6177  opswap  6186  ressn  6242  f1osng  6830  fsng  7088  fsn2g  7089  funopsn  7099  funsneqopb  7103  fnressn  7109  2nd1st  7975  dfmpo  8039  cnvf1olem  8047  xpord2pred  8082  xpord3pred  8089  suppsnop  8114  tpostpos  8182  tfrlem11  8339  naddcllem  8627  ralxpmap  8841  elixpsn  8882  ixpsnf1o  8883  en1b  8974  en1bOLD  8975  mapsnend  8987  xpassen  9017  dif1en  9111  dif1enOLD  9113  en1eqsn  9225  cantnfp1lem3  9625  axdc4lem  10400  ttukeylem3  10456  ttukey2g  10461  fpwwe2lem12  10587  fztp  13507  fzsuc2  13509  fseq1p1m1  13525  fseq1m1p1  13526  expval  13979  hash1elsn  14281  s1val  14498  s1eq  14500  s3sndisj  14864  s3iunsndisj  14865  fsumm1  15647  fprodm1  15861  divalgmod  16299  vdwpc  16863  vdwlem1  16864  vdwlem6  16869  vdwlem7  16870  vdwlem8  16871  cshwsdisj  16982  strle1  17041  setsvalg  17049  setsidvald  17082  setsidvaldOLD  17083  imasval  17407  imasaddvallem  17425  imasvscaval  17434  ismri2dad  17531  mreexd  17536  mreexmrid  17537  homaval  17931  setcmon  17987  funcsetcestrclem1  18056  gsumress  18551  pwsco2mhm  18657  efmnd  18694  idressubmefmnd  18722  smndex1igid  18728  smndex1basss  18729  smndex1mgm  18731  smndex1mndlem  18733  mulgval  18890  idressubgsymg  19206  gsumzaddlem  19712  dmdprd  19791  subgdmdprd  19827  dprdsn  19829  dprd2da  19835  dmdprdpr  19842  dprdpr  19843  dpjfval  19848  dpjval  19849  ablfac1eulem  19865  pgpfaclem1  19874  isunit  20100  isdrng  20229  drngprop  20239  isdrngd  20255  isdrngdOLD  20257  drngpropd  20259  issubdrg  20296  subdrgint  20326  lspsnneg  20524  lspsnsub  20525  lmodindp1  20532  islbs  20594  lspsntrim  20616  lbspropd  20617  lspsnvs  20634  lspsneleq  20635  lspfixed  20648  lpival  20774  zrhrhmb  20948  znval  20975  isobs  21163  frlmval  21191  frlmlbs  21240  islindf  21255  lindfmm  21270  lsslindf  21273  islindf4  21281  islindf5  21282  psrval  21354  mat1dimmul  21862  mat1dimcrng  21863  mat1rhmval  21865  mat1ric  21873  mat1scmat  21925  mdet0pr  21978  m1detdiag  21983  pmatcoe1fsupp  22087  ordtval  22577  ordtcnv  22589  dissnlocfin  22917  ptval2  22989  dfac14  23006  txdis  23020  xkoptsub  23042  pt1hmeo  23194  xpstopnlem1  23197  tgptsmscls  23538  ustuqtoplem  23628  utopsnneiplem  23636  utopsnneip  23637  utop2nei  23639  utop3cls  23640  pcorev2  24428  pcophtb  24429  pi1grplem  24449  pi1inv  24452  cvsunit  24531  i1f1  25091  i1faddlem  25094  i1fmullem  25095  i1fadd  25096  limcfval  25273  dvnfval  25323  ig1pval  25574  0dgrb  25644  dgrnznn  25645  dgreq0  25663  dgrmulc  25669  plyrem  25702  facth  25703  fta1  25705  aaliou2  25737  taylpfval  25761  nosupbnd2lem1  27100  nosupbnd2  27101  noinfbnd2lem1  27115  noinfbnd2  27116  addsproplem3  27326  addsunif  27353  negsproplem3  27371  negsunif  27393  axlowdimlem15  27968  axlowdim  27973  1loopgruspgr  28511  1egrvtxdg1r  28521  1egrvtxdg0  28522  wkslem1  28618  wkslem2  28619  iswlk  28621  redwlk  28683  wlkp1lem8  28691  crctcshwlkn0lem4  28821  crctcshwlkn0lem5  28822  crctcshwlkn0lem6  28823  loopclwwlkn1b  29049  clwwlkn1loopb  29050  clwwlknon1  29104  eupth2lem3lem3  29237  frgrncvvdeqlem3  29308  frgrncvvdeqlem5  29310  wlkl0  29374  0ofval  29792  fcnvgreu  31656  cycpm2tr  32038  lindfpropd  32242  nsgqusf1olem1  32265  elrspunidl  32279  qsidomlem2  32302  rprmval  32337  sradrng  32371  rgmoddim  32392  ply1degltdimlem  32404  dimkerim  32409  irngval  32446  dispcmp  32529  ordtprsval  32588  ordtprsuni  32589  indval2  32702  sitgval  33021  sseqval  33077  reprsuc  33317  lpadval  33378  bnj941  33473  bnj944  33639  revwlk  33805  subfacp1lem5  33865  sconnpht  33910  sconnpht2  33919  sconnpi1  33920  cvmliftlem7  33972  cvmliftlem10  33975  cvmlift2lem13  33996  cvmlift3lem9  34008  satffunlem1lem1  34083  satffunlem2lem1  34085  msrval  34219  mthmpps  34263  onint1  34997  bj-projeq  35536  bj-restsn  35626  finixpnum  36136  matunitlindflem1  36147  ptrest  36150  poimirlem4  36155  poimirlem13  36164  poimirlem14  36165  poimirlem16  36167  poimirlem19  36170  poimirlem26  36177  grpokerinj  36425  isdivrngo  36482  drngoi  36483  isprrngo  36582  lsatset  37525  lsmsat  37543  islshpat  37552  lflsc0N  37618  lkrfval  37622  ldualset  37660  dvafset  39540  dvaset  39541  dvhfset  39616  dvhset  39617  dibffval  39676  dibfval  39677  dib0  39700  cdlemn4a  39735  dihmeetlem4preN  39842  dihmeetlem13N  39855  dih1dimatlem  39865  dihlsprn  39867  dvh2dim  39981  lpolsetN  40018  lclkrlem2j  40052  lclkrlem2p  40058  lcfrlem21  40099  mapdpglem22  40229  mapdpglem23  40230  mapdpglem26  40234  mapdpglem27  40235  mapdpg  40242  baerlem3lem2  40246  baerlem5alem2  40247  baerlem5blem2  40248  baerlem5amN  40252  baerlem5bmN  40253  baerlem5abmN  40254  mapdindp4  40259  mapdhval  40260  mapdheq  40264  mapdh6aN  40271  hvmapffval  40294  hvmapfval  40295  hvmap1o2  40301  hdmap1fval  40332  hdmap1vallem  40333  hdmap1val  40334  hdmap1eq  40337  hdmap1cbv  40338  hdmap1l6a  40345  hdmapfval  40363  hdmap10  40376  hdmaprnlem6N  40390  hgmaprnlem2N  40433  lcmfunnnd  40542  qsalrel  40735  frlmsnic  40786  evlsbagval  40806  prjspval  40999  prjspval2  41009  prjspnvs  41016  prjcrvfval  41027  dfac11  41447  dfac21  41451  nzprmdif  42721  expgrowth  42737  fzdifsuc2  43665  cnrefiisplem  44190  cnrefiisp  44191  hoidmv1le  44955  ovnovollem3  45019  fsetsniunop  45403  fsetsnf  45405  fsetsnf1  45406  fsetsnfo  45407  dfateq12d  45478  otiunsndisjX  45631  funop1  45635  preimafvelsetpreimafv  45700  imaelsetpreimafv  45707  imasetpreimafvbijlemfo  45717  fundcmpsurbijinjpreimafv  45719  fundcmpsurinj  45721  fundcmpsurbijinj  45722  lmod1zr  46694  0aryfvalel  46840  1arymaptf1  46848  mndtcval  47225