Theorem sneqd 4137

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

Syntax hints:   → wi 4   = wceq 1475  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sn 4126

This theorem is referenced by:  otsndisj  4904  otiunsndisj  4905  iunopeqop  4906  dmsnopss  5525  dmsnsnsn  5531  cnvsng  5539  opswap  5540  ressn  5588  f1osng  6089  fsng  6310  fsn2g  6311  funopsn  6319  funsneqopsn  6322  fnressn  6330  fvsng  6352  2nd1st  7104  dfmpt2  7154  cnvf1olem  7162  suppsnop  7196  tpostpos  7259  tfrlem11  7371  ralxpmap  7793  elixpsn  7833  ixpsnf1o  7834  en1b  7910  mapsnen  7920  xpassen  7939  cantnfp1lem3  8460  axdc4lem  9160  ttukeylem3  9216  ttukey2g  9221  fpwwe2lem13  9343  fztp  12267  fzsuc2  12268  fseq1p1m1  12283  fseq1m1p1  12284  expval  12724  s1val  13231  s1eq  13233  s3sndisj  13554  s3iunsndisj  13555  fsumm1  14324  fprodm1  14536  divalgmod  14967  divalgmodOLD  14968  vdwpc  15522  vdwlem1  15523  vdwlem6  15528  vdwlem7  15529  vdwlem8  15530  cshwsdisj  15643  setsvalg  15719  setsidvald  15721  strle1  15800  imasval  15994  imasaddvallem  16012  imasvscaval  16021  ismri2dad  16120  mreexd  16125  mreexmrid  16126  homaval  16504  setcmon  16560  funcsetcestrclem1  16617  gsumress  17099  pwsco2mhm  17194  mulgval  17366  symgval  17622  idressubgsymg  17653  gsumzaddlem  18144  dmdprd  18220  subgdmdprd  18256  dprdsn  18258  dprd2da  18264  dmdprdpr  18271  dprdpr  18272  dpjfval  18277  dpjval  18278  ablfac1eulem  18294  pgpfaclem1  18303  isunit  18480  isdrng  18574  drngprop  18581  isdrngd  18595  drngpropd  18597  issubdrg  18628  lspsnneg  18827  lspsnsub  18828  lmodindp1  18835  islbs  18897  lspsntrim  18919  lbspropd  18920  lspsnvs  18935  lspsneleq  18936  lspfixed  18949  lpival  19066  psrval  19183  zrhrhmb  19678  znval  19702  isobs  19883  frlmval  19911  frlmlbs  19955  islindf  19970  lindfmm  19985  lsslindf  19988  islindf4  19996  islindf5  19997  mat1dimmul  20101  mat1dimcrng  20102  mat1rhmval  20104  mat1ric  20112  mat1scmat  20164  mdet0pr  20217  m1detdiag  20222  pmatcoe1fsupp  20325  ordtval  20803  ordtcnv  20815  dissnlocfin  21142  ptval2  21214  dfac14  21231  txdis  21245  xkoptsub  21267  pt1hmeo  21419  xpstopnlem1  21422  xpstopnlem2  21424  tgptsmscls  21763  ustuqtoplem  21853  utopsnneiplem  21861  utopsnneip  21862  utop2nei  21864  utop3cls  21865  pcorev2  22636  pcophtb  22637  pi1grplem  22657  pi1inv  22660  cvsunit  22739  i1f1  23263  i1faddlem  23266  i1fmullem  23267  i1fadd  23268  limcfval  23442  dvnfval  23491  ig1pval  23736  0dgrb  23806  dgrnznn  23807  dgreq0  23825  dgrmulc  23831  plyrem  23864  facth  23865  fta1  23867  aaliou2  23899  taylpfval  23923  axlowdimlem15  25636  axlowdim  25641  1pthoncl  26122  2pthlem2  26126  eupath2lem3  26506  frgrancvvdeqlem4  26560  frgrancvvdeqlem6  26562  0ofval  27026  fcnvgreu  28855  dispcmp  29254  ordtprsval  29292  ordtprsuni  29293  indval2  29404  sitgval  29721  sseqval  29777  bnj941  30097  bnj944  30262  subfacp1lem5  30420  sconpht  30465  sconpht2  30474  sconpi1  30475  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem13  30551  cvmlift3lem9  30563  msrval  30689  mthmpps  30733  onint1  31618  bj-projeq  32173  bj-restsn  32216  finixpnum  32564  matunitlindflem1  32575  ptrest  32578  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  poimirlem26  32605  grpokerinj  32862  isdivrngo  32919  drngoi  32920  isprrngo  33019  lsatset  33295  lsmsat  33313  islshpat  33322  lflsc0N  33388  lkrfval  33392  ldualset  33430  dvafset  35310  dvaset  35311  dvhfset  35387  dvhset  35388  dibffval  35447  dibfval  35448  dib0  35471  cdlemn4a  35506  dihmeetlem4preN  35613  dihmeetlem13N  35626  dih1dimatlem  35636  dihlsprn  35638  dvh2dim  35752  lpolsetN  35789  lclkrlem2j  35823  lclkrlem2p  35829  lcfrlem21  35870  mapdpglem22  36000  mapdpglem23  36001  mapdpglem26  36005  mapdpglem27  36006  mapdpg  36013  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp4  36030  mapdhval  36031  mapdheq  36035  mapdh6aN  36042  hvmapffval  36065  hvmapfval  36066  hvmap1o2  36072  hdmap1fval  36104  hdmap1vallem  36105  hdmap1val  36106  hdmap1eq  36109  hdmap1cbv  36110  hdmap1l6a  36117  hdmap1neglem1N  36135  hdmapfval  36137  hdmap10  36150  hdmaprnlem6N  36164  hgmaprnlem2N  36207  dfac11  36650  dfac21  36654  nzprmdif  37540  expgrowth  37556  mapsnend  38386  fzdifsuc2  38466  hoidmv1le  39484  ovnovollem3  39548  dfateq12d  39858  otiunsndisjX  40317  funop1  40327  1loopgruspgr  40715  1egrvtxdg1r  40726  1egrvtxdg0  40727  1wlkslem1  40809  1wlkslem2  40810  is1wlk  40813  red1wlk  40881  1wlkp1lem8  40889  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  eupth2lem3lem3  41398  frgrncvvdeqlem4  41472  frgrncvvdeqlem6  41474  lmod1zr  42076