Theorem sneqd 4597

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

Syntax hints:   → wi 4   = wceq 1540  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4586

This theorem is referenced by:  eqsnuniex  5311  otsndisj  5474  otiunsndisj  5475  iunopeqop  5476  dmsnopss  6175  dmsnsnsn  6181  opswap  6190  ressn  6246  suceqd  6387  f1osng  6823  fsng  7091  fsn2g  7092  funopsn  7102  funsneqopb  7106  fnressn  7112  2nd1st  7996  dfmpo  8058  cnvf1olem  8066  xpord2pred  8101  xpord3pred  8108  suppsnop  8134  tpostpos  8202  tfrlem11  8333  naddcllem  8617  ralxpmap  8846  elixpsn  8887  ixpsnf1o  8888  en1b  8973  mapsnend  8984  xpassen  9012  dif1en  9101  dif1enOLD  9103  en1eqsn  9195  cantnfp1lem3  9609  axdc4lem  10384  ttukeylem3  10440  ttukey2g  10445  fpwwe2lem12  10571  fztp  13517  fzsuc2  13519  fseq1p1m1  13535  fseq1m1p1  13536  expval  14004  hash1elsn  14312  s1val  14539  s1eq  14541  s3sndisj  14909  s3iunsndisj  14910  fsumm1  15693  fprodm1  15909  divalgmod  16352  vdwpc  16927  vdwlem1  16928  vdwlem6  16933  vdwlem7  16934  vdwlem8  16935  cshwsdisj  17045  strle1  17104  setsvalg  17112  setsidvald  17145  imasval  17450  imasaddvallem  17468  imasvscaval  17477  ismri2dad  17578  mreexd  17583  mreexmrid  17584  homaval  17973  setcmon  18029  funcsetcestrclem1  18095  gsumress  18591  pwsco2mhm  18742  efmnd  18779  idressubmefmnd  18807  smndex1igid  18813  smndex1basss  18814  smndex1mgm  18816  smndex1mndlem  18818  mulgval  18985  idressubgsymg  19324  gsumzaddlem  19835  dmdprd  19914  subgdmdprd  19950  dprdsn  19952  dprd2da  19958  dmdprdpr  19965  dprdpr  19966  dpjfval  19971  dpjval  19972  ablfac1eulem  19988  pgpfaclem1  19997  isunit  20293  isdrng  20653  drngprop  20664  isdrngd  20685  isdrngdOLD  20687  drngpropd  20689  issubdrg  20700  subdrgint  20723  lspsnneg  20944  lspsnsub  20945  lmodindp1  20952  islbs  21015  lspsntrim  21037  lbspropd  21038  lspsnvs  21056  lspsneleq  21057  lspfixed  21070  rngqiprngimf1  21242  lpival  21266  pzriprnglem13  21435  pzriprnglem14  21436  zrhrhmb  21452  znval  21477  isobs  21662  frlmval  21690  frlmlbs  21739  islindf  21754  lindfmm  21769  lsslindf  21772  islindf4  21780  islindf5  21781  psrval  21857  mat1dimmul  22396  mat1dimcrng  22397  mat1rhmval  22399  mat1ric  22407  mat1scmat  22459  mdet0pr  22512  m1detdiag  22517  pmatcoe1fsupp  22621  ordtval  23109  ordtcnv  23121  dissnlocfin  23449  ptval2  23521  dfac14  23538  txdis  23552  xkoptsub  23574  pt1hmeo  23726  xpstopnlem1  23729  tgptsmscls  24070  ustuqtoplem  24160  utopsnneiplem  24168  utopsnneip  24169  utop2nei  24171  utop3cls  24172  pcorev2  24961  pcophtb  24962  pi1grplem  24982  pi1inv  24985  cvsunit  25064  i1f1  25624  i1faddlem  25627  i1fmullem  25628  i1fadd  25629  limcfval  25806  dvnfval  25857  ig1pval  26114  0dgrb  26184  dgrnznn  26185  dgreq0  26204  dgrmulc  26210  plyrem  26246  facth  26247  fta1  26249  aaliou2  26281  taylpfval  26305  nosupbnd2lem1  27660  nosupbnd2  27661  noinfbnd2lem1  27675  noinfbnd2  27676  eqscut3  27770  addsproplem3  27918  addsuniflem  27948  negsproplem3  27976  negsunif  28001  mulsproplem10  28068  mulsuniflem  28092  n0scut  28266  n0scut2  28267  n0sfincut  28286  zscut  28335  halfcut  28381  addhalfcut  28382  pw2cut  28383  pw2cutp1  28384  zs12bday  28396  axlowdimlem15  28936  axlowdim  28941  1loopgruspgr  29481  1egrvtxdg1r  29491  1egrvtxdg0  29492  wkslem1  29588  wkslem2  29589  iswlk  29591  redwlk  29651  wlkp1lem8  29659  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem6  29795  loopclwwlkn1b  30021  clwwlkn1loopb  30022  clwwlknon1  30076  eupth2lem3lem3  30209  frgrncvvdeqlem3  30280  frgrncvvdeqlem5  30282  wlkl0  30346  0ofval  30766  fcnvgreu  32647  indval2  32827  chnccats1  32987  cycpm2tr  33091  lindfpropd  33346  nsgqusf1olem1  33377  elrspunidl  33392  qsidomlem2  33417  opprqusdrng  33457  rprmval  33480  isufd  33504  pidufd  33507  r1pquslmic  33569  sradrng  33571  rlmdim  33598  rgmoddimOLD  33599  ply1degltdimlem  33611  dimkerim  33616  lvecendof1f1o  33622  irngval  33673  minplym1p  33696  minplynzm1p  33697  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  dispcmp  33842  ordtprsval  33901  ordtprsuni  33902  sitgval  34316  sseqval  34372  reprsuc  34599  lpadval  34660  bnj941  34755  bnj944  34921  revwlk  35105  subfacp1lem5  35164  sconnpht  35209  sconnpht2  35218  sconnpi1  35219  cvmliftlem7  35271  cvmliftlem10  35274  cvmlift2lem13  35295  cvmlift3lem9  35307  satffunlem1lem1  35382  satffunlem2lem1  35384  msrval  35518  mthmpps  35562  onint1  36430  bj-projeq  36973  bj-restsn  37063  finixpnum  37592  matunitlindflem1  37603  ptrest  37606  poimirlem4  37611  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem19  37626  poimirlem26  37633  grpokerinj  37880  isdivrngo  37937  drngoi  37938  isprrngo  38037  lsatset  38976  lsmsat  38994  islshpat  39003  lflsc0N  39069  lkrfval  39073  ldualset  39111  dvafset  40991  dvaset  40992  dvhfset  41067  dvhset  41068  dibffval  41127  dibfval  41128  dib0  41151  cdlemn4a  41186  dihmeetlem4preN  41293  dihmeetlem13N  41306  dih1dimatlem  41316  dihlsprn  41318  dvh2dim  41432  lpolsetN  41469  lclkrlem2j  41503  lclkrlem2p  41509  lcfrlem21  41550  mapdpglem22  41680  mapdpglem23  41681  mapdpglem26  41685  mapdpglem27  41686  mapdpg  41693  baerlem3lem2  41697  baerlem5alem2  41698  baerlem5blem2  41699  baerlem5amN  41703  baerlem5bmN  41704  baerlem5abmN  41705  mapdindp4  41710  mapdhval  41711  mapdheq  41715  mapdh6aN  41722  hvmapffval  41745  hvmapfval  41746  hvmap1o2  41752  hdmap1fval  41783  hdmap1vallem  41784  hdmap1val  41785  hdmap1eq  41788  hdmap1cbv  41789  hdmap1l6a  41796  hdmapfval  41814  hdmap10  41827  hdmaprnlem6N  41841  hgmaprnlem2N  41884  lcmfunnnd  41993  aks6d1c6lem5  42158  qsalrel  42221  frlmsnic  42521  prjspval  42584  prjspval2  42594  prjspnvs  42601  prjcrvfval  42612  dfac11  43044  dfac21  43048  nzprmdif  44301  expgrowth  44317  fzdifsuc2  45301  cnrefiisplem  45820  cnrefiisp  45821  hoidmv1le  46585  ovnovollem3  46649  fsetsniunop  47043  fsetsnf  47045  fsetsnf1  47046  fsetsnfo  47047  dfateq12d  47120  otiunsndisjX  47273  funop1  47277  preimafvelsetpreimafv  47382  imaelsetpreimafv  47389  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  fundcmpsurinj  47403  fundcmpsurbijinj  47404  lmod1zr  48475  0aryfvalel  48616  1arymaptf1  48624  discsubc  49046  imasubclem3  49088  swapf1a  49251  swapf2a  49253  swapf1  49254  swapf2  49256  termcbas2  49464  termchom  49470  termchom2  49471  termcfuncval  49514  mndtcval  49561