MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneq Unicode version

Theorem sneq 4039
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
sneq

Proof of Theorem sneq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2472 . . 3
21abbidv 2593 . 2
3 df-sn 4030 . 2
4 df-sn 4030 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {cab 2442  {csn 4029
This theorem is referenced by:  sneqi  4040  sneqd  4041  euabsn  4102  absneu  4104  preq1  4109  tpeq3  4120  snssg  4163  sneqrg  4199  sneqbg  4200  opeq1  4217  unisng  4265  opthwiener  4754  otiunsndisj  4758  suceq  4948  opeliunxp  5056  relop  5158  elimasng  5368  xpdifid  5440  dmsnsnsn  5491  iotajust  5555  fconstg  5777  f1osng  5859  opabiotafun  5934  fvn0ssdmfun  6022  fsng  6070  fnressn  6083  fressnfv  6085  funfvima3  6149  f12dfv  6179  f13dfv  6180  isofrlem  6236  isoselem  6237  snnex  6606  elxp4  6744  elxp5  6745  1stval  6802  2ndval  6803  2ndval2  6818  fo1st  6820  fo2nd  6821  f1stres  6822  f2ndres  6823  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  fparlem3  6902  fparlem4  6903  suppval  6920  suppsnop  6932  ressuppssdif  6940  brtpos2  6980  dftpos4  6993  tpostpos  6994  eceq1  7366  fvdiagfn  7483  mapsncnv  7485  elixpsn  7528  ixpsnf1o  7529  ensn1g  7600  en1  7602  difsnen  7619  xpsneng  7622  xpcomco  7627  xpassen  7631  xpdom2  7632  canth2  7690  phplem3  7718  xpfi  7811  marypha2lem2  7916  cardsn  8371  pm54.43  8402  dfac5lem3  8527  dfac5lem4  8528  kmlem9  8559  kmlem11  8561  kmlem12  8562  ackbij1lem8  8628  r1om  8645  fictb  8646  hsmexlem4  8830  axcc2lem  8837  axcc2  8838  axdc3lem4  8854  fpwwe2cbv  9029  fpwwe2lem3  9032  fpwwecbv  9043  canth4  9046  fsum2dlem  13585  fsumcnv  13588  fsumcom2  13589  ackbijnn  13640  fprod2dlem  13784  fprodcnv  13787  fprodcom2  13788  xpnnenOLD  13943  vdwlem1  14499  vdwlem12  14510  vdwlem13  14511  vdwnn  14516  0ram  14538  ramz2  14542  pwsval  14883  xpsfval  14964  xpsval  14969  symg2bas  16423  symgfixelsi  16460  pmtrfv  16477  pmtrprfval  16512  sylow2a  16639  efgrelexlema  16767  gsum2dlem2  16998  gsum2dOLD  17000  gsum2d2  17002  gsumcom2  17003  dprdcntz  17041  dprddisj  17042  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  ablfac1eu  17124  ablfaclem3  17138  lssats2  17646  lspsneq0  17658  lbsind  17726  lspsneq  17768  lspdisj2  17773  lspsnsubn0  17786  lspprat  17799  islbs2  17800  lbsextlem4  17807  lbsextg  17808  lpi0  17895  lpi1  17896  psrvsca  18044  evlssca  18191  mpfind  18205  coe1fv  18245  coe1tm  18314  pf1ind  18391  frlmlbs  18831  lindfind  18851  lindsind  18852  lindfrn  18856  submaval  19083  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  islp  19641  perfi  19656  t1sncld  19827  bwth  19910  dis2ndc  19961  nllyi  19976  dissnlocfin  20030  ptbasfi  20082  txkgen  20153  xkofvcn  20185  xkoinjcn  20188  qtopeu  20217  txswaphmeolem  20305  pt1hmeo  20307  elflim2  20465  cnextfvval  20565  cnextcn  20567  cnextfres  20568  tsmsxplem1  20655  tsmsxplem2  20656  ucncn  20788  itg11  22098  i1faddlem  22100  i1fmullem  22101  itg1addlem3  22105  itg1mulc  22111  eldv  22302  ply1lpir  22579  areambl  23288  tglngval  23938  nbgraopALT  24424  nb3graprlem2  24452  cusgrarn  24459  cusgra1v  24461  cusgra2v  24462  cusgra3v  24464  cusgrares  24472  usgrasscusgra  24483  sizeusglecusglem1  24484  uvtxel  24489  cusgrauvtxb  24496  vdgrval  24896  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  1vwmgra  25003  3vfriswmgra  25005  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgrancvvdeqlem4  25033  frgrawopreglem4  25047  frgraregorufr0  25052  2spotiundisj  25062  gxval  25260  h1de2ctlem  26473  spansn  26477  elspansn  26484  elspansn2  26485  spansneleq  26488  h1datom  26500  spansnj  26565  spansncv  26571  superpos  27273  sumdmdlem2  27338  dfcnv2  27517  locfinreflem  27843  sibfima  28280  sibfof  28282  cvmscbv  28703  cvmsdisj  28715  cvmsss2  28719  cvmliftlem15  28743  cvmlift2lem11  28758  cvmlift2lem12  28759  cvmlift2lem13  28760  mvtinf  28915  eldm3  29191  elima4  29209  predeq123  29245  fvsingle  29570  snelsingles  29572  dfiota3  29573  brapply  29588  funpartlem  29592  altopeq12  29612  ranksng  29824  neibastop3  30180  tailval  30191  filnetlem4  30199  heiborlem3  30309  ismrer1  30334  mzpclval  30657  mzpcl1  30661  wopprc  30972  inisegn0  30989  dnnumch3lem  30992  aomclem8  31007  mapfien2OLD  31042  mendvsca  31140  cytpval  31169  dvconstbi  31239  dvmptfprodlem  31741  fourierdlem32  31921  fourierdlem33  31922  fourierdlem48  31937  usgra2pthlem1  32353  irinitoringc  32877  opeliun2xp  32922  dmmpt2ssx2  32926  lindslinindsimp2  33064  ldepspr  33074  ldepsnlinc  33109  bnj1373  34086  bnj1489  34112  lshpnel2N  34710  lsatlspsn2  34717  lsatlspsn  34718  lsatspn0  34725  lkrscss  34823  lfl1dim  34846  lfl1dim2N  34847  ldualvs  34862  atpointN  35467  watvalN  35717  trnsetN  35881  dih1dimatlem  37056  dihatexv  37065  dihjat1lem  37155  dihjat1  37156  lcfl7N  37228  lcfl8  37229  lcfl9a  37232  lcfrlem8  37276  lcfrlem9  37277  lcf1o  37278  mapdval2N  37357  mapdval4N  37359  mapdspex  37395  mapdn0  37396  mapdpglem23  37421  mapdpg  37433  mapdindp1  37447  mapdheq  37455  hvmapval  37487  mapdh9a  37517  hdmap1eq  37529  hdmap1cbv  37530  hdmapval  37558  hdmap10  37570  hdmaplkr  37643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4030
  Copyright terms: Public domain W3C validator