MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneqd Structured version   Visualization version   GIF version

Theorem sneqd 4333
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sneqd (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2 (𝜑𝐴 = 𝐵)
2 sneq 4331 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 17 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  {csn 4321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-sn 4322
This theorem is referenced by:  otsndisj  5129  otiunsndisj  5130  iunopeqop  5131  dmsnopss  5766  dmsnsnsn  5772  cnvsngOLD  5782  opswap  5783  ressn  5832  f1osng  6338  fsng  6567  fsn2g  6568  funopsn  6576  funsneqopsn  6580  fnressn  6588  fvsng  6611  2nd1st  7380  dfmpt2  7435  cnvf1olem  7443  suppsnop  7477  tpostpos  7541  tfrlem11  7653  ralxpmap  8073  elixpsn  8113  ixpsnf1o  8114  en1b  8189  mapsnen  8200  xpassen  8219  cantnfp1lem3  8750  axdc4lem  9469  ttukeylem3  9525  ttukey2g  9530  fpwwe2lem13  9656  fztp  12590  fzsuc2  12591  fseq1p1m1  12607  fseq1m1p1  12608  expval  13056  s1val  13568  s1eq  13570  s3sndisj  13907  s3iunsndisj  13908  fsumm1  14679  fprodm1  14896  divalgmod  15331  divalgmodOLD  15332  vdwpc  15886  vdwlem1  15887  vdwlem6  15892  vdwlem7  15893  vdwlem8  15894  cshwsdisj  16007  setsvalg  16089  setsidvald  16091  strle1  16175  imasval  16373  imasaddvallem  16391  imasvscaval  16400  ismri2dad  16499  mreexd  16504  mreexmrid  16505  homaval  16882  setcmon  16938  funcsetcestrclem1  16995  gsumress  17477  pwsco2mhm  17572  mulgval  17744  symgval  17999  idressubgsymg  18030  gsumzaddlem  18521  dmdprd  18597  subgdmdprd  18633  dprdsn  18635  dprd2da  18641  dmdprdpr  18648  dprdpr  18649  dpjfval  18654  dpjval  18655  ablfac1eulem  18671  pgpfaclem1  18680  isunit  18857  isdrng  18953  drngprop  18960  isdrngd  18974  drngpropd  18976  issubdrg  19007  lspsnneg  19208  lspsnsub  19209  lmodindp1  19216  islbs  19278  lspsntrim  19300  lbspropd  19301  lspsnvs  19316  lspsneleq  19317  lspfixed  19330  lpival  19447  psrval  19564  zrhrhmb  20061  znval  20085  isobs  20266  frlmval  20294  frlmlbs  20338  islindf  20353  lindfmm  20368  lsslindf  20371  islindf4  20379  islindf5  20380  mat1dimmul  20484  mat1dimcrng  20485  mat1rhmval  20487  mat1ric  20495  mat1scmat  20547  mdet0pr  20600  m1detdiag  20605  pmatcoe1fsupp  20708  ordtval  21195  ordtcnv  21207  dissnlocfin  21534  ptval2  21606  dfac14  21623  txdis  21637  xkoptsub  21659  pt1hmeo  21811  xpstopnlem1  21814  xpstopnlem2  21816  tgptsmscls  22154  ustuqtoplem  22244  utopsnneiplem  22252  utopsnneip  22253  utop2nei  22255  utop3cls  22256  pcorev2  23028  pcophtb  23029  pi1grplem  23049  pi1inv  23052  cvsunit  23131  i1f1  23656  i1faddlem  23659  i1fmullem  23660  i1fadd  23661  limcfval  23835  dvnfval  23884  ig1pval  24131  0dgrb  24201  dgrnznn  24202  dgreq0  24220  dgrmulc  24226  plyrem  24259  facth  24260  fta1  24262  aaliou2  24294  taylpfval  24318  axlowdimlem15  26035  axlowdim  26040  1loopgruspgr  26606  1egrvtxdg1r  26616  1egrvtxdg0  26617  wkslem1  26713  wkslem2  26714  iswlk  26716  redwlk  26779  wlkp1lem8  26787  crctcshwlkn0lem4  26916  crctcshwlkn0lem5  26917  crctcshwlkn0lem6  26918  loopclwwlkn1b  27171  clwwlkn1loopb  27172  clwwlknon1  27245  eupth2lem3lem3  27382  frgrncvvdeqlem3  27455  frgrncvvdeqlem5  27457  wlkl0  27528  0ofval  27951  fcnvgreu  29781  dispcmp  30235  ordtprsval  30273  ordtprsuni  30274  indval2  30385  sitgval  30703  sseqval  30759  reprsuc  31002  bnj941  31150  bnj944  31315  subfacp1lem5  31473  sconnpht  31518  sconnpht2  31527  sconnpi1  31528  cvmliftlem7  31580  cvmliftlem10  31583  cvmlift2lem13  31604  cvmlift3lem9  31616  msrval  31742  mthmpps  31786  nosupbnd2lem1  32167  nosupbnd2  32168  onint1  32754  bj-projeq  33286  bj-restsn  33341  finixpnum  33707  matunitlindflem1  33718  ptrest  33721  poimirlem4  33726  poimirlem13  33735  poimirlem14  33736  poimirlem16  33738  poimirlem19  33741  poimirlem26  33748  grpokerinj  34005  isdivrngo  34062  drngoi  34063  isprrngo  34162  lsatset  34780  lsmsat  34798  islshpat  34807  lflsc0N  34873  lkrfval  34877  ldualset  34915  dvafset  36794  dvaset  36795  dvhfset  36871  dvhset  36872  dibffval  36931  dibfval  36932  dib0  36955  cdlemn4a  36990  dihmeetlem4preN  37097  dihmeetlem13N  37110  dih1dimatlem  37120  dihlsprn  37122  dvh2dim  37236  lpolsetN  37273  lclkrlem2j  37307  lclkrlem2p  37313  lcfrlem21  37354  mapdpglem22  37484  mapdpglem23  37485  mapdpglem26  37489  mapdpglem27  37490  mapdpg  37497  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  baerlem5amN  37507  baerlem5bmN  37508  baerlem5abmN  37509  mapdindp4  37514  mapdhval  37515  mapdheq  37519  mapdh6aN  37526  hvmapffval  37549  hvmapfval  37550  hvmap1o2  37556  hdmap1fval  37588  hdmap1vallem  37589  hdmap1val  37590  hdmap1eq  37593  hdmap1cbv  37594  hdmap1l6a  37601  hdmap1neglem1N  37619  hdmapfval  37621  hdmap10  37634  hdmaprnlem6N  37648  hgmaprnlem2N  37691  dfac11  38134  dfac21  38138  nzprmdif  39020  expgrowth  39036  mapsnend  39890  fzdifsuc2  40023  cnrefiisplem  40558  cnrefiisp  40559  hoidmv1le  41314  ovnovollem3  41378  dfateq12d  41715  otiunsndisjX  41806  funop1  41810  lmod1zr  42792
  Copyright terms: Public domain W3C validator