Theorem sneqd 4594

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4583

This theorem is referenced by:  eqsnuniex  5308  otsndisj  5475  otiunsndisj  5476  iunopeqop  5477  dmsnopss  6180  dmsnsnsn  6186  opswap  6195  ressn  6251  suceqd  6392  f1osng  6824  fsng  7092  fsn2g  7093  funopsn  7103  funsneqopb  7107  fnressn  7113  2nd1st  7992  dfmpo  8054  cnvf1olem  8062  xpord2pred  8097  xpord3pred  8104  suppsnop  8130  tpostpos  8198  tfrlem11  8329  naddcllem  8614  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  en1b  8974  mapsnend  8985  xpassen  9011  dif1en  9098  en1eqsn  9187  cantnfp1lem3  9601  axdc4lem  10377  ttukeylem3  10433  ttukey2g  10438  fpwwe2lem12  10565  fztp  13508  fzsuc2  13510  fseq1p1m1  13526  fseq1m1p1  13527  expval  13998  hash1elsn  14306  s1val  14534  s1eq  14536  s3sndisj  14902  s3iunsndisj  14903  fsumm1  15686  fprodm1  15902  divalgmod  16345  vdwpc  16920  vdwlem1  16921  vdwlem6  16926  vdwlem7  16927  vdwlem8  16928  cshwsdisj  17038  strle1  17097  setsvalg  17105  setsidvald  17138  imasval  17444  imasaddvallem  17462  imasvscaval  17471  ismri2dad  17572  mreexd  17577  mreexmrid  17578  homaval  17967  setcmon  18023  funcsetcestrclem1  18089  chnccats1  18560  chnccat  18561  gsumress  18619  pwsco2mhm  18770  efmnd  18807  idressubmefmnd  18835  smndex1igid  18841  smndex1basss  18842  smndex1mgm  18844  smndex1mndlem  18846  mulgval  19013  idressubgsymg  19351  gsumzaddlem  19862  dmdprd  19941  subgdmdprd  19977  dprdsn  19979  dprd2da  19985  dmdprdpr  19992  dprdpr  19993  dpjfval  19998  dpjval  19999  ablfac1eulem  20015  pgpfaclem1  20024  isunit  20321  isdrng  20678  drngprop  20689  isdrngd  20710  isdrngdOLD  20712  drngpropd  20714  issubdrg  20725  subdrgint  20748  lspsnneg  20969  lspsnsub  20970  lmodindp1  20977  islbs  21040  lspsntrim  21062  lbspropd  21063  lspsnvs  21081  lspsneleq  21082  lspfixed  21095  rngqiprngimf1  21267  lpival  21291  pzriprnglem13  21460  pzriprnglem14  21461  zrhrhmb  21477  znval  21502  isobs  21687  frlmval  21715  frlmlbs  21764  islindf  21779  lindfmm  21794  lsslindf  21797  islindf4  21805  islindf5  21806  psrval  21883  mat1dimmul  22432  mat1dimcrng  22433  mat1rhmval  22435  mat1ric  22443  mat1scmat  22495  mdet0pr  22548  m1detdiag  22553  pmatcoe1fsupp  22657  ordtval  23145  ordtcnv  23157  dissnlocfin  23485  ptval2  23557  dfac14  23574  txdis  23588  xkoptsub  23610  pt1hmeo  23762  xpstopnlem1  23765  tgptsmscls  24106  ustuqtoplem  24195  utopsnneiplem  24203  utopsnneip  24204  utop2nei  24206  utop3cls  24207  pcorev2  24996  pcophtb  24997  pi1grplem  25017  pi1inv  25020  cvsunit  25099  i1f1  25659  i1faddlem  25662  i1fmullem  25663  i1fadd  25664  limcfval  25841  dvnfval  25892  ig1pval  26149  0dgrb  26219  dgrnznn  26220  dgreq0  26239  dgrmulc  26245  plyrem  26281  facth  26282  fta1  26284  aaliou2  26316  taylpfval  26340  nosupbnd2lem1  27695  nosupbnd2  27696  noinfbnd2lem1  27710  noinfbnd2  27711  eqcuts3  27812  addsproplem3  27979  addsuniflem  28009  negsproplem3  28038  negsunif  28063  mulsproplem10  28133  mulsuniflem  28157  n0cut  28342  n0cut2  28343  n0fincut  28363  zcuts  28415  halfcut  28466  addhalfcut  28467  pw2cut  28468  pw2cutp1  28469  pw2cut2  28470  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  elreno2  28503  axlowdimlem15  29041  axlowdim  29046  1loopgruspgr  29586  1egrvtxdg1r  29596  1egrvtxdg0  29597  wkslem1  29693  wkslem2  29694  iswlk  29696  redwlk  29756  wlkp1lem8  29764  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  loopclwwlkn1b  30129  clwwlkn1loopb  30130  clwwlknon1  30184  eupth2lem3lem3  30317  frgrncvvdeqlem3  30388  frgrncvvdeqlem5  30390  wlkl0  30454  0ofval  30875  fresunsn  32715  fcnvgreu  32762  indval2  32944  cycpm2tr  33213  lindfpropd  33475  nsgqusf1olem1  33506  elrspunidl  33521  qsidomlem2  33546  opprqusdrng  33586  rprmval  33609  isufd  33633  pidufd  33636  r1pquslmic  33704  extvfvcl  33713  esplyfval0  33741  esplyfval2  33742  esplyind  33752  vieta  33757  sradrng  33759  rlmdim  33787  rgmoddimOLD  33788  ply1degltdimlem  33800  dimkerim  33805  lvecendof1f1o  33811  irngval  33863  extdgfialglem1  33870  minplym1p  33891  minplynzm1p  33892  algextdeglem3  33897  algextdeglem4  33898  algextdeglem5  33899  dispcmp  34037  ordtprsval  34096  ordtprsuni  34097  sitgval  34510  sseqval  34566  reprsuc  34793  lpadval  34854  bnj941  34949  bnj944  35114  revwlk  35341  subfacp1lem5  35400  sconnpht  35445  sconnpht2  35454  sconnpi1  35455  cvmliftlem7  35507  cvmliftlem10  35510  cvmlift2lem13  35531  cvmlift3lem9  35543  satffunlem1lem1  35618  satffunlem2lem1  35620  msrval  35754  mthmpps  35798  onint1  36665  bj-projeq  37240  bj-restsn  37335  finixpnum  37856  matunitlindflem1  37867  ptrest  37870  poimirlem4  37875  poimirlem13  37884  poimirlem14  37885  poimirlem16  37887  poimirlem19  37890  poimirlem26  37897  grpokerinj  38144  isdivrngo  38201  drngoi  38202  isprrngo  38301  lsatset  39366  lsmsat  39384  islshpat  39393  lflsc0N  39459  lkrfval  39463  ldualset  39501  dvafset  41380  dvaset  41381  dvhfset  41456  dvhset  41457  dibffval  41516  dibfval  41517  dib0  41540  cdlemn4a  41575  dihmeetlem4preN  41682  dihmeetlem13N  41695  dih1dimatlem  41705  dihlsprn  41707  dvh2dim  41821  lpolsetN  41858  lclkrlem2j  41892  lclkrlem2p  41898  lcfrlem21  41939  mapdpglem22  42069  mapdpglem23  42070  mapdpglem26  42074  mapdpglem27  42075  mapdpg  42082  baerlem3lem2  42086  baerlem5alem2  42087  baerlem5blem2  42088  baerlem5amN  42092  baerlem5bmN  42093  baerlem5abmN  42094  mapdindp4  42099  mapdhval  42100  mapdheq  42104  mapdh6aN  42111  hvmapffval  42134  hvmapfval  42135  hvmap1o2  42141  hdmap1fval  42172  hdmap1vallem  42173  hdmap1val  42174  hdmap1eq  42177  hdmap1cbv  42178  hdmap1l6a  42185  hdmapfval  42203  hdmap10  42216  hdmaprnlem6N  42230  hgmaprnlem2N  42273  lcmfunnnd  42382  aks6d1c6lem5  42547  qsalrel  42611  frlmsnic  42910  prjspval  42961  prjspval2  42971  prjspnvs  42978  prjcrvfval  42989  dfac11  43419  dfac21  43423  nzprmdif  44675  expgrowth  44691  fzdifsuc2  45672  cnrefiisplem  46187  cnrefiisp  46188  hoidmv1le  46952  ovnovollem3  47016  fsetsniunop  47409  fsetsnf  47411  fsetsnf1  47412  fsetsnfo  47413  dfateq12d  47486  otiunsndisjX  47639  funop1  47643  preimafvelsetpreimafv  47748  imaelsetpreimafv  47755  imasetpreimafvbijlemfo  47765  fundcmpsurbijinjpreimafv  47767  fundcmpsurinj  47769  fundcmpsurbijinj  47770  lmod1zr  48853  0aryfvalel  48994  1arymaptf1  49002  discsubc  49423  imasubclem3  49465  swapf1a  49628  swapf2a  49630  swapf1  49631  swapf2  49633  termcbas2  49841  termchom  49847  termchom2  49848  termcfuncval  49891  mndtcval  49938