Theorem sneqd 4595

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-sn 4588

This theorem is used by:  eqsnuniex  5326  otsndisj  5495  otiunsndisj  5496  iunopeqop  5497  iunopeqopOLD  5498  dmsnopss  6221  dmsnsnsn  6227  opswap  6236  ressn  6294  suceqd  6436  f1osng  6875  fsng  7146  fsn2g  7147  funopsn  7159  funopsnOLD  7160  funsneqopb  7164  fnressn  7170  2nd1st  8056  dfmpo  8123  cnvf1olem  8131  xpord2pred  8172  xpord3pred  8179  suppsnop  8206  tpostpos  8274  tfrlem11  8407  naddcllem  8696  ralxpmap  8935  elixpsn  8976  ixpsnf1o  8977  en1b  9063  mapsnend  9075  xpassen  9101  dif1en  9188  en1eqsn  9277  cantnfp1lem3  9691  axdc4lem  10543  ttukeylem3  10599  ttukey2g  10604  fpwwe2lem12  10737  indval2  12335  fztp  13724  fzsuc2  13726  fseq1p1m1  13742  fseq1m1p1  13743  expval  14216  hash1elsn  14525  s1val  14755  s1eq  14757  s3sndisj  15132  s3iunsndisj  15133  fsumm1  15929  fprodm1  16146  divalgmod  16588  vdwpc  17170  vdwlem1  17171  vdwlem6  17176  vdwlem7  17177  vdwlem8  17178  cshwsdisj  17288  strle1  17348  setsvalg  17356  setsidvald  17389  imasval  17695  imasaddvallem  17713  imasvscaval  17722  ismri2dad  17823  mreexd  17828  mreexmrid  17829  homaval  18218  setcmon  18274  funcsetcestrclem1  18340  chnccats1  18811  chnccat  18812  gsumress  18883  pwsco2mhm  19041  efmnd  19078  idressubmefmnd  19106  smndex1igid  19114  smndex1igidOLD  19115  smndex1basss  19116  smndex1mgm  19118  smndex1mndlem  19120  mulgval  19293  idressubgsymg  19636  gsumzaddlem  20147  dmdprd  20226  subgdmdprd  20262  dprdsn  20264  dprd2da  20270  dmdprdpr  20277  dprdpr  20278  dpjfval  20283  dpjval  20284  ablfac1eulem  20300  pgpfaclem1  20309  isunit  20615  isdrng  20996  drngprop  21010  isdrngd  21034  isdrngdOLD  21036  drngpropd  21039  issubdrg  21049  subdrgint  21072  lspsnneg  21293  lspsnsub  21294  lmodindp1  21301  islbs  21363  lspsntrim  21385  lbspropd  21386  lspsnvs  21404  lspsneleq  21405  lspfixed  21418  rngqiprngimf1  21608  qsidomlem2  21649  lpival  21660  pzriprnglem13  21811  pzriprnglem14  21812  zrhrhmb  21828  znval  21853  isobs  22038  frlmval  22066  frlmlbs  22115  islindf  22130  lindfmm  22145  lsslindf  22148  islindf4  22156  islindf5  22157  psrval  22235  mat1dimmul  22803  mat1dimcrng  22804  mat1rhmval  22806  mat1ric  22814  mat1scmat  22866  mdet0pr  22919  m1detdiag  22924  matunitlindflem1  23006  pmatcoe1fsupp  23031  ordtval  23519  ordtcnv  23531  dissnlocfin  23860  ptval2  23932  dfac14  23949  txdis  23963  xkoptsub  23985  pt1hmeo  24137  xpstopnlem1  24140  tgptsmscls  24481  ustuqtoplem  24570  utopsnneiplem  24578  utopsnneip  24579  utop2nei  24581  utop3cls  24582  pcorev2  25361  pcophtb  25362  pi1grplem  25382  pi1inv  25385  cvsunit  25464  i1f1  26023  i1faddlem  26026  i1fmullem  26027  i1fadd  26028  limcfval  26204  dvnfval  26254  ig1pval  26506  0dgrb  26577  dgrnznn  26578  dgreq0  26596  dgrmulc  26602  plyrem  26638  facth  26639  fta1  26641  aaliou2  26679  taylpfval  26704  nosupbnd2lem1  28084  nosupbnd2  28085  noinfbnd2lem1  28099  noinfbnd2  28100  eqcuts3  28202  addsproplem3  28369  addsuniflem  28399  negsproplem3  28428  negsunif  28453  mulsproplem10  28523  mulsuniflem  28547  n0cut  28732  n0cut2  28733  n0fincut  28753  zcuts  28805  halfcut  28856  addhalfcut  28857  pw2cut  28858  pw2cutp1  28859  pw2cut2  28860  bdaypw2n0bndlem  28861  bdayfinbndlem1  28865  elreno2  28893  axlowdimlem15  29546  axlowdim  29551  1loopgruspgr  30093  1egrvtxdg1r  30103  1egrvtxdg0  30104  wkslem1  30200  wkslem2  30201  iswlk  30203  redwlk  30263  wlkp1lem8  30271  revwlk  30279  crctcshwlkn0lem4  30414  crctcshwlkn0lem5  30415  crctcshwlkn0lem6  30416  loopclwwlkn1b  30645  clwwlkn1loopb  30646  clwwlknon1  30700  eupth2lem3lem3  30843  frgrncvvdeqlem3  30914  frgrncvvdeqlem5  30916  wlkl0  30980  0ofval  31401  fresunsn  33273  fcnvgreu  33320  cycpm2tr  33733  lindfpropd  33990  nsgqusf1olem1  34017  elrspunidl  34031  opprqusdrng  34070  rprmval  34101  isufd  34125  pidufd  34128  r1pquslmic  34195  selvply1rhmlema  34203  selvply1rhmlemb  34204  selvply1rhmlem1  34205  selvply1rhmlem3  34207  selvply1rhmlem5  34209  selvply1rhm  34210  mplidom  34213  extvfvcl  34221  esplyfval0  34249  esplyfval2  34250  esplyind  34260  vieta  34265  sradrng  34267  rlmdim  34295  ply1degltdimlem  34307  dimkerim  34312  lvecendof1f1o  34318  irngval  34370  extdgfialglem1  34377  minplym1p  34398  minplynzm1p  34399  algextdeglem3  34404  algextdeglem4  34405  algextdeglem5  34406  dispcmp  34544  ordtprsval  34603  ordtprsuni  34604  sitgval  35017  sseqval  35073  reprsuc  35297  lpadval  35361  bnj941  35456  bnj944  35621  subfacp1lem5  36070  sconnpht  36115  sconnpht2  36124  sconnpi1  36125  cvmliftlem7  36177  cvmliftlem10  36180  cvmlift2lem13  36201  cvmlift3lem9  36213  satffunlem1lem1  36288  satffunlem2lem1  36290  msrval  36424  mthmpps  36468  onint1  37364  bj-projeq  38032  bj-restsn  38142  finixpnum  38668  ptrest  38677  poimirlem4  38682  poimirlem13  38691  poimirlem14  38692  poimirlem16  38694  poimirlem19  38697  poimirlem26  38704  grpokerinj  38967  isdivrngo  39024  drngoi  39025  isprrngo  39124  lsatset  40187  lsmsat  40205  islshpat  40214  lflsc0N  40280  lkrfval  40284  ldualset  40322  dvafset  42201  dvaset  42202  dvhfset  42277  dvhset  42278  dibffval  42337  dibfval  42338  dib0  42361  cdlemn4a  42396  dihmeetlem4preN  42503  dihmeetlem13N  42516  dih1dimatlem  42526  dihlsprn  42528  dvh2dim  42642  lpolsetN  42679  lclkrlem2j  42713  lclkrlem2p  42719  lcfrlem21  42760  mapdpglem22  42890  mapdpglem23  42891  mapdpglem26  42895  mapdpglem27  42896  mapdpg  42903  baerlem3lem2  42907  baerlem5alem2  42908  baerlem5blem2  42909  baerlem5amN  42913  baerlem5bmN  42914  baerlem5abmN  42915  mapdindp4  42920  mapdhval  42921  mapdheq  42925  mapdh6aN  42932  hvmapffval  42955  hvmapfval  42956  hvmap1o2  42962  hdmap1fval  42993  hdmap1vallem  42994  hdmap1val  42995  hdmap1eq  42998  hdmap1cbv  42999  hdmap1l6a  43006  hdmapfval  43024  hdmap10  43037  hdmaprnlem6N  43051  hgmaprnlem2N  43094  lcmfunnnd  43202  aks6d1c6lem5  43367  qsalrel  43432  frlmsnic  43744  prjspval  43771  prjspval2  43781  prjspnvs  43788  prjcrvfval  43807  dfac11  44204  dfac21  44208  nzprmdif  45443  expgrowth  45459  fzdifsuc2  46465  cnrefiisplem  46978  cnrefiisp  46979  hoidmv1le  47743  ovnovollem3  47807  fsetsniunop  48258  fsetsnf  48260  fsetsnf1  48261  fsetsnfo  48262  dfateq12d  48335  otiunsndisjX  48488  funop1  48492  preimafvelsetpreimafv  48609  imaelsetpreimafv  48616  imasetpreimafvbijlemfo  48626  fundcmpsurbijinjpreimafv  48628  fundcmpsurinj  48630  fundcmpsurbijinj  48631  isprmrng  49572  lmod1zr  49744  0aryfvalel  49885  1arymaptf1  49893  discsubc  50317  imasubclem3  50361  swapf1a  50530  swapf2a  50532  swapf1  50533  swapf2  50535  termcbas2  50756  termchom  50762  termchom2  50763  termcfuncval  50806  termcfunc1eq  50809  mndtcval  50856