Theorem sneqd 4567

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

Syntax hints:   → wi 4   = wceq 1547  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-sn 4556

This theorem is referenced by:  eqsnuniex  5290  otsndisj  5460  otiunsndisj  5461  iunopeqop  5462  iunopeqopOLD  5463  dmsnopss  6165  dmsnsnsn  6171  opswap  6180  ressn  6236  suceqd  6377  f1osng  6809  fsng  7079  fsn2g  7080  funopsn  7090  funopsnOLD  7091  funsneqopb  7095  fnressn  7101  2nd1st  7980  dfmpo  8041  cnvf1olem  8049  xpord2pred  8085  xpord3pred  8092  suppsnop  8118  tpostpos  8186  tfrlem11  8317  naddcllem  8602  ralxpmap  8834  elixpsn  8875  ixpsnf1o  8876  en1b  8962  mapsnend  8973  xpassen  8999  dif1en  9086  en1eqsn  9175  cantnfp1lem3  9592  axdc4lem  10368  ttukeylem3  10424  ttukey2g  10429  fpwwe2lem12  10556  indval2  12155  fztp  13525  fzsuc2  13527  fseq1p1m1  13543  fseq1m1p1  13544  expval  14016  hash1elsn  14324  s1val  14552  s1eq  14554  s3sndisj  14920  s3iunsndisj  14921  fsumm1  15704  fprodm1  15923  divalgmod  16366  vdwpc  16942  vdwlem1  16943  vdwlem6  16948  vdwlem7  16949  vdwlem8  16950  cshwsdisj  17060  strle1  17119  setsvalg  17127  setsidvald  17160  imasval  17466  imasaddvallem  17484  imasvscaval  17493  ismri2dad  17594  mreexd  17599  mreexmrid  17600  homaval  17989  setcmon  18045  funcsetcestrclem1  18111  chnccats1  18582  chnccat  18583  gsumress  18641  pwsco2mhm  18792  efmnd  18829  idressubmefmnd  18857  smndex1igid  18865  smndex1igidOLD  18866  smndex1basss  18867  smndex1mgm  18869  smndex1mndlem  18871  mulgval  19038  idressubgsymg  19376  gsumzaddlem  19887  dmdprd  19966  subgdmdprd  20002  dprdsn  20004  dprd2da  20010  dmdprdpr  20017  dprdpr  20018  dpjfval  20023  dpjval  20024  ablfac1eulem  20040  pgpfaclem1  20049  isunit  20344  isdrng  20705  drngprop  20716  isdrngd  20737  isdrngdOLD  20739  drngpropd  20741  issubdrg  20752  subdrgint  20775  lspsnneg  20996  lspsnsub  20997  lmodindp1  21004  islbs  21066  lspsntrim  21088  lbspropd  21089  lspsnvs  21107  lspsneleq  21108  lspfixed  21121  rngqiprngimf1  21293  lpival  21317  pzriprnglem13  21468  pzriprnglem14  21469  zrhrhmb  21485  znval  21510  isobs  21695  frlmval  21723  frlmlbs  21772  islindf  21787  lindfmm  21802  lsslindf  21805  islindf4  21813  islindf5  21814  psrval  21890  mat1dimmul  22459  mat1dimcrng  22460  mat1rhmval  22462  mat1ric  22470  mat1scmat  22522  mdet0pr  22575  m1detdiag  22580  pmatcoe1fsupp  22684  ordtval  23172  ordtcnv  23184  dissnlocfin  23512  ptval2  23584  dfac14  23601  txdis  23615  xkoptsub  23637  pt1hmeo  23789  xpstopnlem1  23792  tgptsmscls  24133  ustuqtoplem  24222  utopsnneiplem  24230  utopsnneip  24231  utop2nei  24233  utop3cls  24234  pcorev2  25013  pcophtb  25014  pi1grplem  25034  pi1inv  25037  cvsunit  25116  i1f1  25675  i1faddlem  25678  i1fmullem  25679  i1fadd  25680  limcfval  25857  dvnfval  25907  ig1pval  26159  0dgrb  26229  dgrnznn  26230  dgreq0  26248  dgrmulc  26254  plyrem  26289  facth  26290  fta1  26292  aaliou2  26324  taylpfval  26348  nosupbnd2lem1  27697  nosupbnd2  27698  noinfbnd2lem1  27712  noinfbnd2  27713  eqcuts3  27814  addsproplem3  27981  addsuniflem  28011  negsproplem3  28040  negsunif  28065  mulsproplem10  28135  mulsuniflem  28159  n0cut  28344  n0cut2  28345  n0fincut  28365  zcuts  28417  halfcut  28468  addhalfcut  28469  pw2cut  28470  pw2cutp1  28471  pw2cut2  28472  bdaypw2n0bndlem  28473  bdayfinbndlem1  28477  elreno2  28505  axlowdimlem15  29043  axlowdim  29048  1loopgruspgr  29587  1egrvtxdg1r  29597  1egrvtxdg0  29598  wkslem1  29694  wkslem2  29695  iswlk  29697  redwlk  29757  wlkp1lem8  29765  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  loopclwwlkn1b  30130  clwwlkn1loopb  30131  clwwlknon1  30185  eupth2lem3lem3  30318  frgrncvvdeqlem3  30389  frgrncvvdeqlem5  30391  wlkl0  30455  0ofval  30876  fresunsn  32717  fcnvgreu  32764  cycpm2tr  33200  lindfpropd  33465  nsgqusf1olem1  33496  elrspunidl  33511  qsidomlem2  33536  opprqusdrng  33576  rprmval  33599  isufd  33623  pidufd  33626  r1pquslmic  33694  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem3  33706  selvply1rhmlem5  33708  selvply1rhm  33709  mplidom  33712  extvfvcl  33720  esplyfval0  33748  esplyfval2  33749  esplyind  33759  vieta  33764  sradrng  33766  rlmdim  33794  ply1degltdimlem  33806  dimkerim  33811  lvecendof1f1o  33817  irngval  33869  extdgfialglem1  33876  minplym1p  33897  minplynzm1p  33898  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  dispcmp  34043  ordtprsval  34102  ordtprsuni  34103  sitgval  34516  sseqval  34572  reprsuc  34799  lpadval  34860  bnj941  34955  bnj944  35120  revwlk  35353  subfacp1lem5  35412  sconnpht  35457  sconnpht2  35466  sconnpi1  35467  cvmliftlem7  35519  cvmliftlem10  35522  cvmlift2lem13  35543  cvmlift3lem9  35555  satffunlem1lem1  35630  satffunlem2lem1  35632  msrval  35766  mthmpps  35810  onint1  36677  bj-projeq  37345  bj-restsn  37440  finixpnum  37972  matunitlindflem1  37983  ptrest  37986  poimirlem4  37991  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem19  38006  poimirlem26  38013  grpokerinj  38260  isdivrngo  38317  drngoi  38318  isprrngo  38417  lsatset  39482  lsmsat  39500  islshpat  39509  lflsc0N  39575  lkrfval  39579  ldualset  39617  dvafset  41496  dvaset  41497  dvhfset  41572  dvhset  41573  dibffval  41632  dibfval  41633  dib0  41656  cdlemn4a  41691  dihmeetlem4preN  41798  dihmeetlem13N  41811  dih1dimatlem  41821  dihlsprn  41823  dvh2dim  41937  lpolsetN  41974  lclkrlem2j  42008  lclkrlem2p  42014  lcfrlem21  42055  mapdpglem22  42185  mapdpglem23  42186  mapdpglem26  42190  mapdpglem27  42191  mapdpg  42198  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  baerlem5amN  42208  baerlem5bmN  42209  baerlem5abmN  42210  mapdindp4  42215  mapdhval  42216  mapdheq  42220  mapdh6aN  42227  hvmapffval  42250  hvmapfval  42251  hvmap1o2  42257  hdmap1fval  42288  hdmap1vallem  42289  hdmap1val  42290  hdmap1eq  42293  hdmap1cbv  42294  hdmap1l6a  42301  hdmapfval  42319  hdmap10  42332  hdmaprnlem6N  42346  hgmaprnlem2N  42389  lcmfunnnd  42497  aks6d1c6lem5  42662  qsalrel  42725  frlmsnic  43026  prjspval  43053  prjspval2  43063  prjspnvs  43070  prjcrvfval  43081  dfac11  43507  dfac21  43511  nzprmdif  44763  expgrowth  44779  fzdifsuc2  45758  cnrefiisplem  46272  cnrefiisp  46273  hoidmv1le  47037  ovnovollem3  47101  fsetsniunop  47512  fsetsnf  47514  fsetsnf1  47515  fsetsnfo  47516  dfateq12d  47589  otiunsndisjX  47742  funop1  47746  preimafvelsetpreimafv  47863  imaelsetpreimafv  47870  imasetpreimafvbijlemfo  47880  fundcmpsurbijinjpreimafv  47882  fundcmpsurinj  47884  fundcmpsurbijinj  47885  lmod1zr  48984  0aryfvalel  49125  1arymaptf1  49133  discsubc  49554  imasubclem3  49596  swapf1a  49759  swapf2a  49761  swapf1  49762  swapf2  49764  termcbas2  49972  termchom  49978  termchom2  49979  termcfuncval  50022  mndtcval  50069