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

Theorem ssid 3367
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
ssid  |-  A  C_  A

Proof of Theorem ssid
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 id 20 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3352 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  eqimssi  3402  eqimss2i  3403  nsspssun  3574  inv1  3654  disjpss  3678  difid  3696  pwidg  3811  elssuni  4043  unimax  4049  intmin  4070  rintn0  4181  ordunidif  4629  iunpw  4759  onsucuni  4808  tfisi  4838  xpss1  4984  xpss2  4985  residm  5177  resdm  5184  resmpt3  5192  ssrnres  5309  dffn3  5598  fimacnv  5862  fparlem3  6448  fparlem4  6449  tfrlem1  6636  tz7.48-2  6699  abianfp  6716  oaordi  6789  omwordi  6814  omass  6823  nnaordi  6861  nnmwordi  6878  fpmg  7039  boxcutc  7105  domss2  7266  0fin  7336  en1eqsn  7338  fimax2g  7353  domunfican  7379  pwfi  7402  fissuni  7411  fipreima  7412  wofib  7514  wemapso  7520  sucprcreg  7567  noinfep  7614  noinfepOLD  7615  cantnfval2  7624  cantnfp1lem3  7636  tcidm  7685  tc0  7686  r1rankidb  7730  r1pw  7771  rankr1id  7788  scott0  7810  htalem  7820  xpomen  7897  infpwfien  7943  alephsmo  7983  dfac12lem3  8025  ackbij2lem4  8122  cflem  8126  cflecard  8133  cflim2  8143  cfslb  8146  fin4en1  8189  fin23lem13  8212  fin23lem15  8214  fin23lem36  8228  isf32lem1  8233  fin67  8275  dcomex  8327  zorn2lem4  8379  alephexp2  8456  fpwwe2lem13  8517  canthnumlem  8523  wunex2  8613  wuncidm  8621  eltsk2g  8626  axgroth6  8703  axgroth3  8706  xrsup  11249  expcl  11399  hashcard  11638  hashf1lem2  11705  lo1eq  12362  rlimeq  12363  serclim0  12371  isercolllem2  12459  isercoll  12461  summolem3  12508  isum  12513  fsumser  12524  fsumcl  12527  fsum2d  12555  fsumabs  12580  fsumrlim  12590  fsumo1  12591  fsumiun  12600  flo1  12634  eflt  12718  xpnnenOLD  12809  rpnnen2lem3  12816  rpnnen2lem5  12818  rpnnen2lem11  12824  rpnnen2  12825  rexpen  12827  eulerthlem2  13171  ressid  13524  ressinbas  13525  mremre  13829  yon11  14361  yon12  14362  yon2  14363  yonpropd  14365  oppcyon  14366  yonffth  14381  p0le  14472  ple1  14473  oduclatb  14571  ipopos  14586  fpwipodrs  14590  submid  14751  mulgnncl  14905  mulgnn0cl  14906  mulgcl  14907  subgid  14946  cntrnsg  15140  sylow3lem5  15265  lsmss1  15298  lsmss2  15300  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumadd  15528  gsumzsplit  15529  gsumzmhm  15533  gsumzoppg  15539  gsumzinv  15540  gsumsub  15542  gsum2d  15546  dprdfinv  15577  dprdf1  15591  dmdprdsplitlem  15595  dprd2db  15601  dpjidcl  15616  ablfac1eulem  15630  ablfac1eu  15631  ablfaclem2  15644  gsumdixp  15715  subrgid  15870  lss1  16015  lbsextlem1  16230  rlmbas  16267  rlmplusg  16268  rlm0  16269  rlmmulr  16270  rlmsca  16271  rlmsca2  16272  rlmvsca  16273  rlmtopn  16274  rlmds  16275  psrass1lem  16442  mplsubglem  16498  mpllsslem  16499  mplsubrglem  16502  mplcoe1  16528  mplbas2  16531  evlslem4  16564  psrbagev1  16566  evlslem2  16568  znf1o  16832  zntoslem  16837  css0  16916  topopn  16979  fiinbas  17017  topbas  17037  topcld  17099  clstop  17133  ntrtop  17134  opnneissb  17178  opnssneib  17179  opnneiid  17190  neiptopuni  17194  neiptoptop  17195  maxlp  17211  isperf2  17216  restopn2  17241  restperf  17248  idcn  17321  cnconst2  17347  lmres  17364  rncmp  17459  fiuncmp  17467  cmpfi  17471  concn  17489  1stcelcls  17524  llyidm  17551  nllyidm  17552  toplly  17553  kgentopon  17570  kgencn2  17589  ptpjpre1  17603  ptbasfi  17613  ptcld  17645  xkopt  17687  elqtop2  17733  qtopuni  17734  ptcmpfi  17845  fbssfi  17869  opnfbas  17874  filtop  17887  isfil2  17888  isfild  17890  fsubbas  17899  ssfg  17904  filssufilg  17943  ufileu  17951  imaelfm  17983  rnelfm  17985  fmfnfmlem4  17989  neiflim  18006  supnfcls  18052  fclscf  18057  flimfnfcls  18060  tsmsfbas  18157  utopbas  18265  xpsxmet  18410  xpsdsval  18411  xpsmet  18412  tmsxms  18516  tmsms  18517  imasf1oxms  18519  imasf1oms  18520  prdsxms  18560  prdsms  18561  tmsxpsval  18568  retopbas  18794  cnngp  18814  cnperf  18851  retopcon  18860  fsumcn  18900  abscncf  18931  recncf  18932  imcncf  18933  cjcncf  18934  mulc1cncf  18935  cncfcn1  18940  cncfmpt2f  18944  cncfmpt2ss  18945  addccncf  18946  cdivcncf  18947  negcncf  18948  negfcncf  18949  abscncfALT  18950  cnmpt2pc  18953  xrhmeo  18971  oprpiece1res1  18976  oprpiece1res2  18977  cnrehmeo  18978  iscau3  19231  caubl  19260  caublcls  19261  evthicc2  19357  ovolre  19421  volsuplem  19449  uniiccdif  19470  uniioovol  19471  uniiccvol  19472  uniioombllem3  19477  uniioombllem4  19478  uniioombllem5  19479  dyadmbllem  19491  volcn  19498  volivth  19499  itgfsum  19718  iblabslem  19719  iblabs  19720  bddmulibl  19730  cnlimc  19775  cnlimci  19776  dvres3  19800  dvres3a  19801  dvidlem  19802  dvcnp2  19806  dvcn  19807  dvnadd  19815  dvnres  19817  cpnord  19821  cpnres  19823  dvaddbr  19824  dvmulbr  19825  dvcmul  19830  dvcmulf  19831  dvcobr  19832  dvcjbr  19835  dvrec  19841  dvmptntr  19857  dvmptfsum  19859  dveflem  19863  dvef  19864  rolle  19874  dvlipcn  19878  c1liplem1  19880  dvgt0lem2  19887  dvivth  19894  lhop1lem  19897  dvfsumabs  19907  ftc1a  19921  ftc1cn  19927  ftc2  19928  deg1mul3le  20039  plyssc  20119  plyeq0  20130  coeeulem  20143  0dgr  20164  coemulc  20173  coe0  20174  coesub  20175  coe1termlem  20176  dgrmulc  20189  dgrsub  20190  dgrcolem1  20191  dgrcolem2  20192  dvnply2  20204  plycpn  20206  plyremlem  20221  fta1lem  20224  vieta1lem2  20228  aalioulem3  20251  dvntaylp  20287  taylthlem1  20289  taylthlem2  20290  ulmcn  20315  psercn  20342  pserdv  20345  abelth  20357  efcn  20359  efcvx  20365  pige3  20425  dvrelog  20528  logcn  20538  dvloglem  20539  dvlog  20542  dvlog2  20544  efopnlem2  20548  logccv  20554  cxpcn  20629  cxpcn2  20630  cxpcn3  20632  resqrcn  20633  sqrcn  20634  loglesqr  20642  atancn  20776  rlimcnp3  20806  jensen  20827  ftalem3  20857  basellem2  20864  dchrfi  21039  dchrisumlema  21182  pntrsumo1  21259  pntrsumbnd  21260  pntlem3  21303  cusgrasizeindslem2  21483  efghgrp  21961  sspid  22224  ssps  22229  helch  22746  hhssnv  22764  hhsssh  22769  shintcl  22832  chintcl  22834  shlesb1i  22888  omlsi  22906  chlejb1i  22978  chm0i  22992  chabs1  23018  chabs2  23019  spanun  23047  cmidi  23112  pjidmcoi  23680  csmdsymi  23837  sumdmdlem2  23922  dmdbr5ati  23925  mdcompli  23932  dmdcompli  23933  disjdifprg  24017  fdmrn  24039  xppreima  24059  xrinfm  24121  clatp0ex  24193  clatp1ex  24194  xrsmulgzz  24200  xrsp0  24203  xrsp1  24204  pnfneige0  24336  esumsn  24456  esumcvg  24476  pwsiga  24513  sigagenid  24534  lgamgulmlem2  24814  cvmlift2lem6  24995  relexpdm  25135  relexprn  25136  rtrclreclem.refl  25144  rtrclreclem.subset  25145  prodmolem3  25259  iprod  25264  iprodn0  25266  fprodss  25274  fprodcl  25278  fprod2d  25305  risefaccl  25331  fallfaccl  25332  trpredtr  25508  trpredpo  25513  wzel  25575  frrlem5c  25588  frrlem10  25593  imagesset  25798  ontgval  26181  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  mbfposadd  26254  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anc  26288  ftc2nc  26289  areacirclem2  26293  areacirclem3  26294  areacirclem4  26295  areacirc  26297  ivthALT  26338  fness  26362  ssref  26363  fneref  26364  refref  26365  refssfne  26374  fnemeet1  26395  fnejoin2  26398  filnetlem2  26408  filnetlem4  26410  welb  26438  caures  26466  constcncf  26468  idcncf  26469  sub1cncf  26470  sub2cncf  26471  cnresima  26473  rngoidl  26634  ralxpmap  26742  lcomfsup  26747  ismrcd1  26752  ismrc  26755  incssnn0  26765  mzpclall  26784  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  expdioph  27094  aomclem6  27134  kelac1  27138  frlmsslsp  27225  frlmlbs  27226  frlmup1  27227  gicabl  27240  rgspnid  27354  symggen  27388  lhe4.4ex1a  27523  dvsconst  27524  dvsid  27525  dvsef  27526  dvconstbi  27528  dvcosre  27717  itgsinexplem1  27724  funresfunco  27965  onfrALTlem3  28630  onfrALTlem3VD  28999  bnj1253  29386  atpsubN  30550  pol1N  30707  1psubclN  30741  cdlemefrs32fva  31197  dia2dimlem13  31874  dibord  31957  dochvalr  32155  hdmapevec  32636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator