Theorem sneqd 4484

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

Syntax hints:   → wi 4   = wceq 1522  {csn 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-sn 4473

This theorem is referenced by:  otsndisj  5300  otiunsndisj  5301  iunopeqop  5302  dmsnopss  5946  dmsnsnsn  5952  opswap  5961  ressn  6011  f1osng  6523  fsng  6762  fsn2g  6763  funopsn  6773  funsneqopb  6777  fnressn  6783  fvsngOLD  6808  2nd1st  7593  dfmpo  7653  cnvf1olem  7661  suppsnop  7695  tpostpos  7763  tfrlem11  7876  ralxpmap  8309  elixpsn  8349  ixpsnf1o  8350  en1b  8425  mapsnend  8436  xpassen  8458  cantnfp1lem3  8989  axdc4lem  9723  ttukeylem3  9779  ttukey2g  9784  fpwwe2lem13  9910  fztp  12813  fzsuc2  12815  fseq1p1m1  12831  fseq1m1p1  12832  expval  13281  s1val  13796  s1eq  13798  s3sndisj  14161  s3iunsndisj  14162  fsumm1  14939  fprodm1  15154  divalgmod  15590  vdwpc  16145  vdwlem1  16146  vdwlem6  16151  vdwlem7  16152  vdwlem8  16153  cshwsdisj  16261  setsvalg  16341  setsidvald  16343  strle1  16421  imasval  16613  imasaddvallem  16631  imasvscaval  16640  ismri2dad  16737  mreexd  16742  mreexmrid  16743  homaval  17120  setcmon  17176  funcsetcestrclem1  17233  gsumress  17715  pwsco2mhm  17810  mulgval  17985  symgval  18238  idressubgsymg  18269  gsumzaddlem  18761  dmdprd  18837  subgdmdprd  18873  dprdsn  18875  dprd2da  18881  dmdprdpr  18888  dprdpr  18889  dpjfval  18894  dpjval  18895  ablfac1eulem  18911  pgpfaclem1  18920  isunit  19097  isdrng  19196  drngprop  19203  isdrngd  19217  drngpropd  19219  issubdrg  19250  subdrgint  19272  lspsnneg  19468  lspsnsub  19469  lmodindp1  19476  islbs  19538  lspsntrim  19560  lbspropd  19561  lspsnvs  19576  lspsneleq  19577  lspfixed  19590  lpival  19707  psrval  19830  zrhrhmb  20340  znval  20364  isobs  20546  frlmval  20574  frlmlbs  20623  islindf  20638  lindfmm  20653  lsslindf  20656  islindf4  20664  islindf5  20665  mat1dimmul  20769  mat1dimcrng  20770  mat1rhmval  20772  mat1ric  20780  mat1scmat  20832  mdet0pr  20885  m1detdiag  20890  pmatcoe1fsupp  20993  ordtval  21481  ordtcnv  21493  dissnlocfin  21821  ptval2  21893  dfac14  21910  txdis  21924  xkoptsub  21946  pt1hmeo  22098  xpstopnlem1  22101  tgptsmscls  22441  ustuqtoplem  22531  utopsnneiplem  22539  utopsnneip  22540  utop2nei  22542  utop3cls  22543  pcorev2  23315  pcophtb  23316  pi1grplem  23336  pi1inv  23339  cvsunit  23418  i1f1  23974  i1faddlem  23977  i1fmullem  23978  i1fadd  23979  limcfval  24153  dvnfval  24202  ig1pval  24449  0dgrb  24519  dgrnznn  24520  dgreq0  24538  dgrmulc  24544  plyrem  24577  facth  24578  fta1  24580  aaliou2  24612  taylpfval  24636  axlowdimlem15  26425  axlowdim  26430  1loopgruspgr  26965  1egrvtxdg1r  26975  1egrvtxdg0  26976  wkslem1  27072  wkslem2  27073  iswlk  27075  redwlk  27139  wlkp1lem8  27147  crctcshwlkn0lem4  27278  crctcshwlkn0lem5  27279  crctcshwlkn0lem6  27280  loopclwwlkn1b  27507  clwwlkn1loopb  27508  clwwlknon1  27563  eupth2lem3lem3  27697  frgrncvvdeqlem3  27772  frgrncvvdeqlem5  27774  wlkl0  27838  0ofval  28255  fcnvgreu  30108  cycpm2tr  30408  lindfpropd  30588  sradrng  30592  rgmoddim  30612  dimkerim  30627  dispcmp  30740  ordtprsval  30778  ordtprsuni  30779  indval2  30890  sitgval  31207  sseqval  31263  reprsuc  31503  lpadval  31564  bnj941  31661  bnj944  31826  subfacp1lem5  32039  sconnpht  32084  sconnpht2  32093  sconnpi1  32094  cvmliftlem7  32146  cvmliftlem10  32149  cvmlift2lem13  32170  cvmlift3lem9  32182  satffunlem1lem1  32257  satffunlem2lem1  32259  msrval  32393  mthmpps  32437  nosupbnd2lem1  32824  nosupbnd2  32825  onint1  33406  bj-projeq  33909  bj-restsn  33972  finixpnum  34408  matunitlindflem1  34419  ptrest  34422  poimirlem4  34427  poimirlem13  34436  poimirlem14  34437  poimirlem16  34439  poimirlem19  34442  poimirlem26  34449  grpokerinj  34703  isdivrngo  34760  drngoi  34761  isprrngo  34860  lsatset  35657  lsmsat  35675  islshpat  35684  lflsc0N  35750  lkrfval  35754  ldualset  35792  dvafset  37671  dvaset  37672  dvhfset  37747  dvhset  37748  dibffval  37807  dibfval  37808  dib0  37831  cdlemn4a  37866  dihmeetlem4preN  37973  dihmeetlem13N  37986  dih1dimatlem  37996  dihlsprn  37998  dvh2dim  38112  lpolsetN  38149  lclkrlem2j  38183  lclkrlem2p  38189  lcfrlem21  38230  mapdpglem22  38360  mapdpglem23  38361  mapdpglem26  38365  mapdpglem27  38366  mapdpg  38373  baerlem3lem2  38377  baerlem5alem2  38378  baerlem5blem2  38379  baerlem5amN  38383  baerlem5bmN  38384  baerlem5abmN  38385  mapdindp4  38390  mapdhval  38391  mapdheq  38395  mapdh6aN  38402  hvmapffval  38425  hvmapfval  38426  hvmap1o2  38432  hdmap1fval  38463  hdmap1vallem  38464  hdmap1val  38465  hdmap1eq  38468  hdmap1cbv  38469  hdmap1l6a  38476  hdmapfval  38494  hdmap10  38507  hdmaprnlem6N  38521  hgmaprnlem2N  38564  qsalrel  38655  frlmsnic  38676  prjspval  38750  prjspval2  38760  dfac11  39147  dfac21  39151  hash1elsn  40057  nzprmdif  40189  expgrowth  40205  fzdifsuc2  41118  cnrefiisplem  41652  cnrefiisp  41653  hoidmv1le  42418  ovnovollem3  42482  dfateq12d  42841  otiunsndisjX  42994  funop1  42998  lmod1zr  44028