Theorem sneqd 4189

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

Syntax hints:   → wi 4   = wceq 1483  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sn 4178

This theorem is referenced by:  otsndisj  4979  otiunsndisj  4980  iunopeqop  4981  dmsnopss  5607  dmsnsnsn  5613  cnvsng  5621  opswap  5622  ressn  5671  f1osng  6177  fsng  6404  fsn2g  6405  funopsn  6413  funsneqopsn  6417  fnressn  6425  fvsng  6447  2nd1st  7213  dfmpt2  7267  cnvf1olem  7275  suppsnop  7309  tpostpos  7372  tfrlem11  7484  ralxpmap  7907  elixpsn  7947  ixpsnf1o  7948  en1b  8024  mapsnen  8035  xpassen  8054  cantnfp1lem3  8577  axdc4lem  9277  ttukeylem3  9333  ttukey2g  9338  fpwwe2lem13  9464  fztp  12397  fzsuc2  12398  fseq1p1m1  12414  fseq1m1p1  12415  expval  12862  s1val  13378  s1eq  13380  s3sndisj  13706  s3iunsndisj  13707  fsumm1  14480  fprodm1  14697  divalgmod  15129  divalgmodOLD  15130  vdwpc  15684  vdwlem1  15685  vdwlem6  15690  vdwlem7  15691  vdwlem8  15692  cshwsdisj  15805  setsvalg  15887  setsidvald  15889  strle1  15973  imasval  16171  imasaddvallem  16189  imasvscaval  16198  ismri2dad  16297  mreexd  16302  mreexmrid  16303  homaval  16681  setcmon  16737  funcsetcestrclem1  16794  gsumress  17276  pwsco2mhm  17371  mulgval  17543  symgval  17799  idressubgsymg  17830  gsumzaddlem  18321  dmdprd  18397  subgdmdprd  18433  dprdsn  18435  dprd2da  18441  dmdprdpr  18448  dprdpr  18449  dpjfval  18454  dpjval  18455  ablfac1eulem  18471  pgpfaclem1  18480  isunit  18657  isdrng  18751  drngprop  18758  isdrngd  18772  drngpropd  18774  issubdrg  18805  lspsnneg  19006  lspsnsub  19007  lmodindp1  19014  islbs  19076  lspsntrim  19098  lbspropd  19099  lspsnvs  19114  lspsneleq  19115  lspfixed  19128  lpival  19245  psrval  19362  zrhrhmb  19859  znval  19883  isobs  20064  frlmval  20092  frlmlbs  20136  islindf  20151  lindfmm  20166  lsslindf  20169  islindf4  20177  islindf5  20178  mat1dimmul  20282  mat1dimcrng  20283  mat1rhmval  20285  mat1ric  20293  mat1scmat  20345  mdet0pr  20398  m1detdiag  20403  pmatcoe1fsupp  20506  ordtval  20993  ordtcnv  21005  dissnlocfin  21332  ptval2  21404  dfac14  21421  txdis  21435  xkoptsub  21457  pt1hmeo  21609  xpstopnlem1  21612  xpstopnlem2  21614  tgptsmscls  21953  ustuqtoplem  22043  utopsnneiplem  22051  utopsnneip  22052  utop2nei  22054  utop3cls  22055  pcorev2  22828  pcophtb  22829  pi1grplem  22849  pi1inv  22852  cvsunit  22931  i1f1  23457  i1faddlem  23460  i1fmullem  23461  i1fadd  23462  limcfval  23636  dvnfval  23685  ig1pval  23932  0dgrb  24002  dgrnznn  24003  dgreq0  24021  dgrmulc  24027  plyrem  24060  facth  24061  fta1  24063  aaliou2  24095  taylpfval  24119  axlowdimlem15  25836  axlowdim  25841  1loopgruspgr  26396  1egrvtxdg1r  26406  1egrvtxdg0  26407  wkslem1  26503  wkslem2  26504  iswlk  26506  redwlk  26569  wlkp1lem8  26577  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  eupth2lem3lem3  27090  frgrncvvdeqlem3  27165  frgrncvvdeqlem5  27167  0ofval  27642  fcnvgreu  29472  dispcmp  29926  ordtprsval  29964  ordtprsuni  29965  indval2  30076  sitgval  30394  sseqval  30450  reprsuc  30693  bnj941  30843  bnj944  31008  subfacp1lem5  31166  sconnpht  31211  sconnpht2  31220  sconnpi1  31221  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem13  31297  cvmlift3lem9  31309  msrval  31435  mthmpps  31479  nosupbnd2lem1  31861  nosupbnd2  31862  onint1  32448  bj-projeq  32980  bj-restsn  33035  finixpnum  33394  matunitlindflem1  33405  ptrest  33408  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  poimirlem26  33435  grpokerinj  33692  isdivrngo  33749  drngoi  33750  isprrngo  33849  lsatset  34277  lsmsat  34295  islshpat  34304  lflsc0N  34370  lkrfval  34374  ldualset  34412  dvafset  36292  dvaset  36293  dvhfset  36369  dvhset  36370  dibffval  36429  dibfval  36430  dib0  36453  cdlemn4a  36488  dihmeetlem4preN  36595  dihmeetlem13N  36608  dih1dimatlem  36618  dihlsprn  36620  dvh2dim  36734  lpolsetN  36771  lclkrlem2j  36805  lclkrlem2p  36811  lcfrlem21  36852  mapdpglem22  36982  mapdpglem23  36983  mapdpglem26  36987  mapdpglem27  36988  mapdpg  36995  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdindp4  37012  mapdhval  37013  mapdheq  37017  mapdh6aN  37024  hvmapffval  37047  hvmapfval  37048  hvmap1o2  37054  hdmap1fval  37086  hdmap1vallem  37087  hdmap1val  37088  hdmap1eq  37091  hdmap1cbv  37092  hdmap1l6a  37099  hdmap1neglem1N  37117  hdmapfval  37119  hdmap10  37132  hdmaprnlem6N  37146  hgmaprnlem2N  37189  dfac11  37632  dfac21  37636  nzprmdif  38518  expgrowth  38534  mapsnend  39391  fzdifsuc2  39525  cnrefiisplem  40055  cnrefiisp  40056  hoidmv1le  40808  ovnovollem3  40872  dfateq12d  41209  otiunsndisjX  41298  funop1  41302  lmod1zr  42282