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

Theorem sneqd 4222
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 4220 . 2 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2syl 17 1 (𝜑 → {𝐴} = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sn 4211
This theorem is referenced by:  otsndisj  5008  otiunsndisj  5009  iunopeqop  5010  dmsnopss  5643  dmsnsnsn  5649  cnvsngOLD  5659  opswap  5660  ressn  5709  f1osng  6215  fsng  6444  fsn2g  6445  funopsn  6453  funsneqopsn  6457  fnressn  6465  fvsng  6488  2nd1st  7257  dfmpt2  7312  cnvf1olem  7320  suppsnop  7354  tpostpos  7417  tfrlem11  7529  ralxpmap  7949  elixpsn  7989  ixpsnf1o  7990  en1b  8065  mapsnen  8076  xpassen  8095  cantnfp1lem3  8615  axdc4lem  9315  ttukeylem3  9371  ttukey2g  9376  fpwwe2lem13  9502  fztp  12435  fzsuc2  12436  fseq1p1m1  12452  fseq1m1p1  12453  expval  12902  s1val  13414  s1eq  13416  s3sndisj  13752  s3iunsndisj  13753  fsumm1  14524  fprodm1  14741  divalgmod  15176  divalgmodOLD  15177  vdwpc  15731  vdwlem1  15732  vdwlem6  15737  vdwlem7  15738  vdwlem8  15739  cshwsdisj  15852  setsvalg  15934  setsidvald  15936  strle1  16020  imasval  16218  imasaddvallem  16236  imasvscaval  16245  ismri2dad  16344  mreexd  16349  mreexmrid  16350  homaval  16728  setcmon  16784  funcsetcestrclem1  16841  gsumress  17323  pwsco2mhm  17418  mulgval  17590  symgval  17845  idressubgsymg  17876  gsumzaddlem  18367  dmdprd  18443  subgdmdprd  18479  dprdsn  18481  dprd2da  18487  dmdprdpr  18494  dprdpr  18495  dpjfval  18500  dpjval  18501  ablfac1eulem  18517  pgpfaclem1  18526  isunit  18703  isdrng  18799  drngprop  18806  isdrngd  18820  drngpropd  18822  issubdrg  18853  lspsnneg  19054  lspsnsub  19055  lmodindp1  19062  islbs  19124  lspsntrim  19146  lbspropd  19147  lspsnvs  19162  lspsneleq  19163  lspfixed  19176  lpival  19293  psrval  19410  zrhrhmb  19907  znval  19931  isobs  20112  frlmval  20140  frlmlbs  20184  islindf  20199  lindfmm  20214  lsslindf  20217  islindf4  20225  islindf5  20226  mat1dimmul  20330  mat1dimcrng  20331  mat1rhmval  20333  mat1ric  20341  mat1scmat  20393  mdet0pr  20446  m1detdiag  20451  pmatcoe1fsupp  20554  ordtval  21041  ordtcnv  21053  dissnlocfin  21380  ptval2  21452  dfac14  21469  txdis  21483  xkoptsub  21505  pt1hmeo  21657  xpstopnlem1  21660  xpstopnlem2  21662  tgptsmscls  22000  ustuqtoplem  22090  utopsnneiplem  22098  utopsnneip  22099  utop2nei  22101  utop3cls  22102  pcorev2  22874  pcophtb  22875  pi1grplem  22895  pi1inv  22898  cvsunit  22977  i1f1  23502  i1faddlem  23505  i1fmullem  23506  i1fadd  23507  limcfval  23681  dvnfval  23730  ig1pval  23977  0dgrb  24047  dgrnznn  24048  dgreq0  24066  dgrmulc  24072  plyrem  24105  facth  24106  fta1  24108  aaliou2  24140  taylpfval  24164  axlowdimlem15  25881  axlowdim  25886  1loopgruspgr  26452  1egrvtxdg1r  26462  1egrvtxdg0  26463  wkslem1  26559  wkslem2  26560  iswlk  26562  redwlk  26625  wlkp1lem8  26633  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  loopclwwlkn1b  27005  clwwlkn1loopb  27006  clwwlknon1  27072  eupth2lem3lem3  27208  frgrncvvdeqlem3  27281  frgrncvvdeqlem5  27283  0ofval  27770  fcnvgreu  29600  dispcmp  30054  ordtprsval  30092  ordtprsuni  30093  indval2  30204  sitgval  30522  sseqval  30578  reprsuc  30821  bnj941  30969  bnj944  31134  subfacp1lem5  31292  sconnpht  31337  sconnpht2  31346  sconnpi1  31347  cvmliftlem7  31399  cvmliftlem10  31402  cvmlift2lem13  31423  cvmlift3lem9  31435  msrval  31561  mthmpps  31605  nosupbnd2lem1  31986  nosupbnd2  31987  onint1  32573  bj-projeq  33105  bj-restsn  33160  finixpnum  33524  matunitlindflem1  33535  ptrest  33538  poimirlem4  33543  poimirlem13  33552  poimirlem14  33553  poimirlem16  33555  poimirlem19  33558  poimirlem26  33565  grpokerinj  33822  isdivrngo  33879  drngoi  33880  isprrngo  33979  lsatset  34595  lsmsat  34613  islshpat  34622  lflsc0N  34688  lkrfval  34692  ldualset  34730  dvafset  36609  dvaset  36610  dvhfset  36686  dvhset  36687  dibffval  36746  dibfval  36747  dib0  36770  cdlemn4a  36805  dihmeetlem4preN  36912  dihmeetlem13N  36925  dih1dimatlem  36935  dihlsprn  36937  dvh2dim  37051  lpolsetN  37088  lclkrlem2j  37122  lclkrlem2p  37128  lcfrlem21  37169  mapdpglem22  37299  mapdpglem23  37300  mapdpglem26  37304  mapdpglem27  37305  mapdpg  37312  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdindp4  37329  mapdhval  37330  mapdheq  37334  mapdh6aN  37341  hvmapffval  37364  hvmapfval  37365  hvmap1o2  37371  hdmap1fval  37403  hdmap1vallem  37404  hdmap1val  37405  hdmap1eq  37408  hdmap1cbv  37409  hdmap1l6a  37416  hdmap1neglem1N  37434  hdmapfval  37436  hdmap10  37449  hdmaprnlem6N  37463  hgmaprnlem2N  37506  dfac11  37949  dfac21  37953  nzprmdif  38835  expgrowth  38851  mapsnend  39705  fzdifsuc2  39838  cnrefiisplem  40373  cnrefiisp  40374  hoidmv1le  41129  ovnovollem3  41193  dfateq12d  41530  otiunsndisjX  41621  funop1  41625  lmod1zr  42607
  Copyright terms: Public domain W3C validator