Theorem sneqd 4590

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-sn 4579

This theorem is referenced by:  eqsnuniex  5304  otsndisj  5465  otiunsndisj  5466  iunopeqop  5467  dmsnopss  6170  dmsnsnsn  6176  opswap  6185  ressn  6241  suceqd  6382  f1osng  6814  fsng  7080  fsn2g  7081  funopsn  7091  funsneqopb  7095  fnressn  7101  2nd1st  7980  dfmpo  8042  cnvf1olem  8050  xpord2pred  8085  xpord3pred  8092  suppsnop  8118  tpostpos  8186  tfrlem11  8317  naddcllem  8602  ralxpmap  8832  elixpsn  8873  ixpsnf1o  8874  en1b  8960  mapsnend  8971  xpassen  8997  dif1en  9084  en1eqsn  9173  cantnfp1lem3  9587  axdc4lem  10363  ttukeylem3  10419  ttukey2g  10424  fpwwe2lem12  10551  fztp  13494  fzsuc2  13496  fseq1p1m1  13512  fseq1m1p1  13513  expval  13984  hash1elsn  14292  s1val  14520  s1eq  14522  s3sndisj  14888  s3iunsndisj  14889  fsumm1  15672  fprodm1  15888  divalgmod  16331  vdwpc  16906  vdwlem1  16907  vdwlem6  16912  vdwlem7  16913  vdwlem8  16914  cshwsdisj  17024  strle1  17083  setsvalg  17091  setsidvald  17124  imasval  17430  imasaddvallem  17448  imasvscaval  17457  ismri2dad  17558  mreexd  17563  mreexmrid  17564  homaval  17953  setcmon  18009  funcsetcestrclem1  18075  chnccats1  18546  chnccat  18547  gsumress  18605  pwsco2mhm  18756  efmnd  18793  idressubmefmnd  18821  smndex1igid  18827  smndex1basss  18828  smndex1mgm  18830  smndex1mndlem  18832  mulgval  18999  idressubgsymg  19337  gsumzaddlem  19848  dmdprd  19927  subgdmdprd  19963  dprdsn  19965  dprd2da  19971  dmdprdpr  19978  dprdpr  19979  dpjfval  19984  dpjval  19985  ablfac1eulem  20001  pgpfaclem1  20010  isunit  20307  isdrng  20664  drngprop  20675  isdrngd  20696  isdrngdOLD  20698  drngpropd  20700  issubdrg  20711  subdrgint  20734  lspsnneg  20955  lspsnsub  20956  lmodindp1  20963  islbs  21026  lspsntrim  21048  lbspropd  21049  lspsnvs  21067  lspsneleq  21068  lspfixed  21081  rngqiprngimf1  21253  lpival  21277  pzriprnglem13  21446  pzriprnglem14  21447  zrhrhmb  21463  znval  21488  isobs  21673  frlmval  21701  frlmlbs  21750  islindf  21765  lindfmm  21780  lsslindf  21783  islindf4  21791  islindf5  21792  psrval  21869  mat1dimmul  22418  mat1dimcrng  22419  mat1rhmval  22421  mat1ric  22429  mat1scmat  22481  mdet0pr  22534  m1detdiag  22539  pmatcoe1fsupp  22643  ordtval  23131  ordtcnv  23143  dissnlocfin  23471  ptval2  23543  dfac14  23560  txdis  23574  xkoptsub  23596  pt1hmeo  23748  xpstopnlem1  23751  tgptsmscls  24092  ustuqtoplem  24181  utopsnneiplem  24189  utopsnneip  24190  utop2nei  24192  utop3cls  24193  pcorev2  24982  pcophtb  24983  pi1grplem  25003  pi1inv  25006  cvsunit  25085  i1f1  25645  i1faddlem  25648  i1fmullem  25649  i1fadd  25650  limcfval  25827  dvnfval  25878  ig1pval  26135  0dgrb  26205  dgrnznn  26206  dgreq0  26225  dgrmulc  26231  plyrem  26267  facth  26268  fta1  26270  aaliou2  26302  taylpfval  26326  nosupbnd2lem1  27681  nosupbnd2  27682  noinfbnd2lem1  27696  noinfbnd2  27697  eqscut3  27792  addsproplem3  27941  addsuniflem  27971  negsproplem3  27999  negsunif  28024  mulsproplem10  28094  mulsuniflem  28118  n0scut  28294  n0scut2  28295  n0sfincut  28315  zscut  28365  halfcut  28415  addhalfcut  28416  pw2cut  28417  pw2cutp1  28418  pw2cut2  28419  bdaypw2n0s  28420  zs12bday  28433  elreno2  28440  axlowdimlem15  28978  axlowdim  28983  1loopgruspgr  29523  1egrvtxdg1r  29533  1egrvtxdg0  29534  wkslem1  29630  wkslem2  29631  iswlk  29633  redwlk  29693  wlkp1lem8  29701  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  loopclwwlkn1b  30066  clwwlkn1loopb  30067  clwwlknon1  30121  eupth2lem3lem3  30254  frgrncvvdeqlem3  30325  frgrncvvdeqlem5  30327  wlkl0  30391  0ofval  30811  fresunsn  32652  fcnvgreu  32700  indval2  32882  cycpm2tr  33150  lindfpropd  33412  nsgqusf1olem1  33443  elrspunidl  33458  qsidomlem2  33483  opprqusdrng  33523  rprmval  33546  isufd  33570  pidufd  33573  r1pquslmic  33641  extvfvcl  33650  esplyfval0  33671  esplyfval2  33672  esplyind  33680  vieta  33685  sradrng  33687  rlmdim  33715  rgmoddimOLD  33716  ply1degltdimlem  33728  dimkerim  33733  lvecendof1f1o  33739  irngval  33791  extdgfialglem1  33798  minplym1p  33819  minplynzm1p  33820  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  dispcmp  33965  ordtprsval  34024  ordtprsuni  34025  sitgval  34438  sseqval  34494  reprsuc  34721  lpadval  34782  bnj941  34877  bnj944  35043  revwlk  35268  subfacp1lem5  35327  sconnpht  35372  sconnpht2  35381  sconnpi1  35382  cvmliftlem7  35434  cvmliftlem10  35437  cvmlift2lem13  35458  cvmlift3lem9  35470  satffunlem1lem1  35545  satffunlem2lem1  35547  msrval  35681  mthmpps  35725  onint1  36592  bj-projeq  37136  bj-restsn  37226  finixpnum  37745  matunitlindflem1  37756  ptrest  37759  poimirlem4  37764  poimirlem13  37773  poimirlem14  37774  poimirlem16  37776  poimirlem19  37779  poimirlem26  37786  grpokerinj  38033  isdivrngo  38090  drngoi  38091  isprrngo  38190  lsatset  39189  lsmsat  39207  islshpat  39216  lflsc0N  39282  lkrfval  39286  ldualset  39324  dvafset  41203  dvaset  41204  dvhfset  41279  dvhset  41280  dibffval  41339  dibfval  41340  dib0  41363  cdlemn4a  41398  dihmeetlem4preN  41505  dihmeetlem13N  41518  dih1dimatlem  41528  dihlsprn  41530  dvh2dim  41644  lpolsetN  41681  lclkrlem2j  41715  lclkrlem2p  41721  lcfrlem21  41762  mapdpglem22  41892  mapdpglem23  41893  mapdpglem26  41897  mapdpglem27  41898  mapdpg  41905  baerlem3lem2  41909  baerlem5alem2  41910  baerlem5blem2  41911  baerlem5amN  41915  baerlem5bmN  41916  baerlem5abmN  41917  mapdindp4  41922  mapdhval  41923  mapdheq  41927  mapdh6aN  41934  hvmapffval  41957  hvmapfval  41958  hvmap1o2  41964  hdmap1fval  41995  hdmap1vallem  41996  hdmap1val  41997  hdmap1eq  42000  hdmap1cbv  42001  hdmap1l6a  42008  hdmapfval  42026  hdmap10  42039  hdmaprnlem6N  42053  hgmaprnlem2N  42096  lcmfunnnd  42205  aks6d1c6lem5  42370  qsalrel  42438  frlmsnic  42737  prjspval  42788  prjspval2  42798  prjspnvs  42805  prjcrvfval  42816  dfac11  43246  dfac21  43250  nzprmdif  44502  expgrowth  44518  fzdifsuc2  45500  cnrefiisplem  46015  cnrefiisp  46016  hoidmv1le  46780  ovnovollem3  46844  fsetsniunop  47237  fsetsnf  47239  fsetsnf1  47240  fsetsnfo  47241  dfateq12d  47314  otiunsndisjX  47467  funop1  47471  preimafvelsetpreimafv  47576  imaelsetpreimafv  47583  imasetpreimafvbijlemfo  47593  fundcmpsurbijinjpreimafv  47595  fundcmpsurinj  47597  fundcmpsurbijinj  47598  lmod1zr  48681  0aryfvalel  48822  1arymaptf1  48830  discsubc  49251  imasubclem3  49293  swapf1a  49456  swapf2a  49458  swapf1  49459  swapf2  49461  termcbas2  49669  termchom  49675  termchom2  49676  termcfuncval  49719  mndtcval  49766