Theorem sneqd 4596

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-sn 4585

This theorem is used by:  eqsnuniex  5326  otsndisj  5496  otiunsndisj  5497  iunopeqop  5498  iunopeqopOLD  5499  dmsnopss  6210  dmsnsnsn  6216  opswap  6225  ressn  6283  suceqd  6425  f1osng  6861  fsng  7132  fsn2g  7133  funopsn  7145  funopsnOLD  7146  funsneqopb  7150  fnressn  7156  2nd1st  8036  dfmpo  8100  cnvf1olem  8108  xpord2pred  8144  xpord3pred  8151  suppsnop  8177  tpostpos  8245  tfrlem11  8378  naddcllem  8665  ralxpmap  8904  elixpsn  8945  ixpsnf1o  8946  en1b  9032  mapsnend  9044  xpassen  9070  dif1en  9157  en1eqsn  9246  cantnfp1lem3  9660  axdc4lem  10458  ttukeylem3  10514  ttukey2g  10519  fpwwe2lem12  10652  indval2  12248  fztp  13636  fzsuc2  13638  fseq1p1m1  13654  fseq1m1p1  13655  expval  14128  hash1elsn  14436  s1val  14666  s1eq  14668  s3sndisj  15041  s3iunsndisj  15042  fsumm1  15838  fprodm1  16055  divalgmod  16497  vdwpc  17073  vdwlem1  17074  vdwlem6  17079  vdwlem7  17080  vdwlem8  17081  cshwsdisj  17191  strle1  17251  setsvalg  17259  setsidvald  17292  imasval  17598  imasaddvallem  17616  imasvscaval  17625  ismri2dad  17726  mreexd  17731  mreexmrid  17732  homaval  18121  setcmon  18177  funcsetcestrclem1  18243  chnccats1  18714  chnccat  18715  gsumress  18785  pwsco2mhm  18943  efmnd  18980  idressubmefmnd  19008  smndex1igid  19016  smndex1igidOLD  19017  smndex1basss  19018  smndex1mgm  19020  smndex1mndlem  19022  mulgval  19195  idressubgsymg  19538  gsumzaddlem  20049  dmdprd  20128  subgdmdprd  20164  dprdsn  20166  dprd2da  20172  dmdprdpr  20179  dprdpr  20180  dpjfval  20185  dpjval  20186  ablfac1eulem  20202  pgpfaclem1  20211  isunit  20515  isdrng  20895  drngprop  20908  isdrngd  20932  isdrngdOLD  20934  drngpropd  20937  issubdrg  20947  subdrgint  20970  lspsnneg  21191  lspsnsub  21192  lmodindp1  21199  islbs  21261  lspsntrim  21283  lbspropd  21284  lspsnvs  21302  lspsneleq  21303  lspfixed  21316  rngqiprngimf1  21504  qsidomlem2  21545  lpival  21556  pzriprnglem13  21707  pzriprnglem14  21708  zrhrhmb  21724  znval  21749  isobs  21934  frlmval  21962  frlmlbs  22011  islindf  22026  lindfmm  22041  lsslindf  22044  islindf4  22052  islindf5  22053  psrval  22131  mat1dimmul  22699  mat1dimcrng  22700  mat1rhmval  22702  mat1ric  22710  mat1scmat  22762  mdet0pr  22815  m1detdiag  22820  matunitlindflem1  22902  pmatcoe1fsupp  22927  ordtval  23415  ordtcnv  23427  dissnlocfin  23756  ptval2  23828  dfac14  23845  txdis  23859  xkoptsub  23881  pt1hmeo  24033  xpstopnlem1  24036  tgptsmscls  24377  ustuqtoplem  24466  utopsnneiplem  24474  utopsnneip  24475  utop2nei  24477  utop3cls  24478  pcorev2  25257  pcophtb  25258  pi1grplem  25278  pi1inv  25281  cvsunit  25360  i1f1  25919  i1faddlem  25922  i1fmullem  25923  i1fadd  25924  limcfval  26100  dvnfval  26150  ig1pval  26402  0dgrb  26473  dgrnznn  26474  dgreq0  26492  dgrmulc  26498  plyrem  26536  facth  26537  fta1  26539  aaliou2  26577  taylpfval  26602  nosupbnd2lem1  27952  nosupbnd2  27953  noinfbnd2lem1  27967  noinfbnd2  27968  eqcuts3  28070  addsproplem3  28237  addsuniflem  28267  negsproplem3  28296  negsunif  28321  mulsproplem10  28391  mulsuniflem  28415  n0cut  28600  n0cut2  28601  n0fincut  28621  zcuts  28673  halfcut  28724  addhalfcut  28725  pw2cut  28726  pw2cutp1  28727  pw2cut2  28728  bdaypw2n0bndlem  28729  bdayfinbndlem1  28733  elreno2  28761  axlowdimlem15  29414  axlowdim  29419  1loopgruspgr  29961  1egrvtxdg1r  29971  1egrvtxdg0  29972  wkslem1  30068  wkslem2  30069  iswlk  30071  redwlk  30131  wlkp1lem8  30139  revwlk  30147  crctcshwlkn0lem4  30282  crctcshwlkn0lem5  30283  crctcshwlkn0lem6  30284  loopclwwlkn1b  30513  clwwlkn1loopb  30514  clwwlknon1  30568  eupth2lem3lem3  30711  frgrncvvdeqlem3  30782  frgrncvvdeqlem5  30784  wlkl0  30848  0ofval  31269  fresunsn  33099  fcnvgreu  33146  cycpm2tr  33560  lindfpropd  33816  nsgqusf1olem1  33843  elrspunidl  33857  opprqusdrng  33896  rprmval  33927  isufd  33951  pidufd  33954  r1pquslmic  34021  selvply1rhmlema  34029  selvply1rhmlemb  34030  selvply1rhmlem1  34031  selvply1rhmlem3  34033  selvply1rhmlem5  34035  selvply1rhm  34036  mplidom  34039  extvfvcl  34047  esplyfval0  34075  esplyfval2  34076  esplyind  34086  vieta  34091  sradrng  34093  rlmdim  34121  ply1degltdimlem  34133  dimkerim  34138  lvecendof1f1o  34144  irngval  34196  extdgfialglem1  34203  minplym1p  34224  minplynzm1p  34225  algextdeglem3  34230  algextdeglem4  34231  algextdeglem5  34232  dispcmp  34370  ordtprsval  34429  ordtprsuni  34430  sitgval  34844  sseqval  34900  reprsuc  35124  lpadval  35188  bnj941  35283  bnj944  35448  subfacp1lem5  35764  sconnpht  35809  sconnpht2  35818  sconnpi1  35819  cvmliftlem7  35871  cvmliftlem10  35874  cvmlift2lem13  35895  cvmlift3lem9  35907  satffunlem1lem1  35982  satffunlem2lem1  35984  msrval  36118  mthmpps  36162  onint1  37069  bj-projeq  37737  bj-restsn  37833  finixpnum  38360  ptrest  38369  poimirlem4  38374  poimirlem13  38383  poimirlem14  38384  poimirlem16  38386  poimirlem19  38389  poimirlem26  38396  grpokerinj  38644  isdivrngo  38701  drngoi  38702  isprrngo  38801  lsatset  39864  lsmsat  39882  islshpat  39891  lflsc0N  39957  lkrfval  39961  ldualset  39999  dvafset  41878  dvaset  41879  dvhfset  41954  dvhset  41955  dibffval  42014  dibfval  42015  dib0  42038  cdlemn4a  42073  dihmeetlem4preN  42180  dihmeetlem13N  42193  dih1dimatlem  42203  dihlsprn  42205  dvh2dim  42319  lpolsetN  42356  lclkrlem2j  42390  lclkrlem2p  42396  lcfrlem21  42437  mapdpglem22  42567  mapdpglem23  42568  mapdpglem26  42572  mapdpglem27  42573  mapdpg  42580  baerlem3lem2  42584  baerlem5alem2  42585  baerlem5blem2  42586  baerlem5amN  42590  baerlem5bmN  42591  baerlem5abmN  42592  mapdindp4  42597  mapdhval  42598  mapdheq  42602  mapdh6aN  42609  hvmapffval  42632  hvmapfval  42633  hvmap1o2  42639  hdmap1fval  42670  hdmap1vallem  42671  hdmap1val  42672  hdmap1eq  42675  hdmap1cbv  42676  hdmap1l6a  42683  hdmapfval  42701  hdmap10  42714  hdmaprnlem6N  42728  hgmaprnlem2N  42771  lcmfunnnd  42879  aks6d1c6lem5  43044  qsalrel  43109  frlmsnic  43423  prjspval  43450  prjspval2  43460  prjspnvs  43467  prjcrvfval  43478  dfac11  43904  dfac21  43908  nzprmdif  45144  expgrowth  45160  fzdifsuc2  46144  cnrefiisplem  46658  cnrefiisp  46659  hoidmv1le  47423  ovnovollem3  47487  fsetsniunop  47938  fsetsnf  47940  fsetsnf1  47941  fsetsnfo  47942  dfateq12d  48015  otiunsndisjX  48168  funop1  48172  preimafvelsetpreimafv  48289  imaelsetpreimafv  48296  imasetpreimafvbijlemfo  48306  fundcmpsurbijinjpreimafv  48308  fundcmpsurinj  48310  fundcmpsurbijinj  48311  isprmrng  49252  lmod1zr  49424  0aryfvalel  49565  1arymaptf1  49573  discsubc  49991  imasubclem3  50033  swapf1a  50196  swapf2a  50198  swapf1  50199  swapf2  50201  termcbas2  50409  termchom  50415  termchom2  50416  termcfuncval  50459  mndtcval  50506