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

Theorem ssid 3118
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
StepHypRef Expression
1 id 21 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3105 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3078
This theorem is referenced by:  eqimssi  3153  eqimss2i  3154  nsspssun  3309  inv1  3388  disjpss  3412  difid  3428  pwidg  3541  elssuni  3753  unimax  3759  intmin  3780  rintn0  3890  ordunidif  4333  iunpw  4461  onsucuni  4510  tfisi  4540  xpss1  4702  xpss2  4703  residm  4893  resdm  4900  resmpt3  4908  ssrnres  5023  dffn3  5253  fimacnv  5509  fparlem3  6072  fparlem4  6073  tfrlem1  6277  tz7.48-2  6340  abianfp  6357  oaordi  6430  omwordi  6455  omass  6464  nnaordi  6502  nnmwordi  6519  fpmg  6679  boxcutc  6745  domss2  6905  0fin  6972  en1eqsn  6973  fimax2g  6988  domunfican  7014  pwfi  7035  fissuni  7044  fipreima  7045  wofib  7144  wemapso  7150  sucprcreg  7197  noinfep  7244  noinfepOLD  7245  cantnfval2  7254  cantnfp1lem3  7266  tcidm  7315  tc0  7316  r1rankidb  7360  r1pw  7401  rankr1id  7418  scott0  7440  htalem  7450  xpomen  7527  infpwfien  7573  alephsmo  7613  dfac12lem3  7655  ackbij2lem4  7752  cflem  7756  cflecard  7763  cflim2  7773  cfslb  7776  fin4en1  7819  fin23lem13  7842  fin23lem15  7844  fin23lem36  7858  isf32lem1  7863  fin67  7905  dcomex  7957  zorn2lem4  8010  alephexp2  8083  fpwwe2lem13  8144  canthnumlem  8150  wunex2  8240  wuncidm  8248  eltsk2g  8253  axgroth6  8330  axgroth3  8333  xrsup  10850  expcl  10999  hashcard  11227  hashf1lem2  11271  lo1eq  11919  rlimeq  11920  serclim0  11928  isercolllem2  12016  isercoll  12018  summolem3  12064  isum  12069  fsumser  12080  fsumcl  12083  fsum2d  12111  fsumabs  12136  fsumrlim  12146  fsumo1  12147  fsumiun  12156  flo1  12187  eflt  12271  xpnnenOLD  12362  rpnnen2lem3  12369  rpnnen2lem5  12371  rpnnen2lem11  12377  rpnnen2  12378  rexpen  12380  eulerthlem2  12724  ressid  13077  ressinbas  13078  mremre  13378  yon11  13882  yon12  13883  yon2  13884  yonpropd  13886  oppcyon  13887  yonffth  13902  p0le  13993  ple1  13994  oduclatb  14092  ipopos  14107  fpwipodrs  14111  submid  14263  mulgnncl  14417  mulgnn0cl  14418  mulgcl  14419  subgid  14458  cntrnsg  14652  sylow3lem5  14777  lsmss1  14810  lsmss2  14812  gsumzres  15029  gsumzcl  15030  gsumzf1o  15031  gsumadd  15040  gsumzsplit  15041  gsumzmhm  15045  gsumzoppg  15051  gsumzinv  15052  gsumsub  15054  gsum2d  15058  dprdfinv  15089  dprdf1  15103  dmdprdsplitlem  15107  dprd2db  15113  dpjidcl  15128  ablfac1eulem  15142  ablfac1eu  15143  ablfaclem2  15156  gsumdixp  15227  subrgid  15382  lss1  15531  lbsextlem1  15743  rlmbas  15780  rlmplusg  15781  rlm0  15782  rlmmulr  15783  rlmsca  15784  rlmsca2  15785  rlmvsca  15786  rlmtopn  15787  rlmds  15788  psrass1lem  15955  mplsubglem  16011  mpllsslem  16012  mplsubrglem  16015  mplcoe1  16041  mplbas2  16044  evlslem4  16077  psrbagev1  16079  evlslem2  16081  znf1o  16337  zntoslem  16342  css0  16421  topopn  16484  fiinbas  16522  topbas  16542  topcld  16604  clstop  16638  ntrtop  16639  opnneissb  16683  opnssneib  16684  opnneiid  16695  maxlp  16710  isperf2  16715  restopn2  16740  restperf  16746  idcn  16819  cnconst2  16843  lmres  16860  rncmp  16955  fiuncmp  16963  cmpfi  16967  concn  16984  1stcelcls  17019  llyidm  17046  nllyidm  17047  toplly  17048  kgentopon  17065  kgencn2  17084  ptpjpre1  17098  ptbasfi  17108  ptcld  17139  xkopt  17181  elqtop2  17224  qtopuni  17225  ptcmpfi  17336  fbssfi  17364  opnfbas  17369  filtop  17382  isfil2  17383  isfild  17385  fsubbas  17394  ssfg  17399  filssufilg  17438  ufileu  17446  imaelfm  17478  rnelfm  17480  fmfnfmlem4  17484  neiflim  17501  supnfcls  17547  fclscf  17552  flimfnfcls  17555  tsmsfbas  17642  xpsxmet  17776  xpsdsval  17777  xpsmet  17778  tmsxms  17864  tmsms  17865  imasf1oxms  17867  imasf1oms  17868  prdsxms  17908  prdsms  17909  tmsxpsval  17916  retopbas  18101  cnngp  18121  cnperf  18157  retopcon  18166  fsumcn  18206  abscncf  18237  recncf  18238  imcncf  18239  cjcncf  18240  mulc1cncf  18241  cncfcn1  18246  cncfmpt2f  18250  cncfmpt2ss  18251  cdivcncf  18252  negcncf  18253  negfcncf  18254  abscncfALT  18255  cnmpt2pc  18258  xrhmeo  18276  oprpiece1res1  18281  oprpiece1res2  18282  cnrehmeo  18283  iscau3  18536  caubl  18565  caublcls  18566  evthicc2  18652  ovolre  18716  volsuplem  18744  uniiccdif  18765  uniioovol  18766  uniiccvol  18767  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  dyadmbllem  18786  volcn  18793  volivth  18794  itgfsum  19013  iblabslem  19014  iblabs  19015  bddmulibl  19025  cnlimc  19070  cnlimci  19071  dvres3  19095  dvres3a  19096  dvidlem  19097  dvcnp2  19101  dvcn  19102  dvnadd  19110  dvnres  19112  cpnord  19116  cpnres  19118  dvaddbr  19119  dvmulbr  19120  dvcmul  19125  dvcmulf  19126  dvcobr  19127  dvcjbr  19130  dvrec  19136  dvmptntr  19152  dvmptfsum  19154  dveflem  19158  dvef  19159  rolle  19169  dvlipcn  19173  c1liplem1  19175  dvgt0lem2  19182  dvivth  19189  lhop1lem  19192  dvfsumabs  19202  ftc1a  19216  ftc1cn  19222  ftc2  19223  deg1mul3le  19334  plyssc  19414  plyeq0  19425  coeeulem  19438  0dgr  19459  coemulc  19468  coe0  19469  coesub  19470  coe1termlem  19471  dgrmulc  19484  dgrsub  19485  dgrcolem1  19486  dgrcolem2  19487  dvnply2  19499  plycpn  19501  plyremlem  19516  fta1lem  19519  vieta1lem2  19523  aalioulem3  19546  dvntaylp  19582  taylthlem1  19584  taylthlem2  19585  ulmcn  19608  psercn  19634  pserdv  19637  abelth  19649  efcn  19651  efcvx  19657  pige3  19717  dvrelog  19816  logcn  19826  dvloglem  19827  dvlog  19830  dvlog2  19832  efopnlem2  19836  logccv  19842  cxpcn  19953  cxpcn2  19954  cxpcn3  19956  resqrcn  19957  sqrcn  19958  loglesqr  19966  atancn  20064  rlimcnp3  20094  jensen  20115  ftalem3  20144  basellem2  20151  dchrfi  20326  dchrisumlema  20469  pntrsumo1  20546  pntrsumbnd  20547  pntlem3  20590  efghgrp  20870  sspid  21131  ssps  21136  helch  21653  hhssnv  21671  hhsssh  21676  shintcl  21739  chintcl  21741  shlesb1i  21795  omlsi  21813  chlejb1i  21885  chm0i  21899  chabs1  21925  chabs2  21926  spanun  21954  cmidi  22037  pjidmcoi  22587  csmdsymi  22744  sumdmdlem2  22829  dmdbr5ati  22832  mdcompli  22839  dmdcompli  22840  cvmlift2lem6  23010  relexpdm  23203  relexprn  23204  rtrclreclem.refl  23212  rtrclreclem.subset  23213  trpredtr  23401  trpredpo  23406  frrlem5c  23455  frrlem10  23460  ontgval  24044  residcp  24242  prl2  24335  inpc  24443  inposet  24444  dominc  24446  rninc  24447  domncnt  24448  ranncnt  24449  dfps2  24455  toplat  24456  fsumprd  24495  clfsebs  24513  fincmpzer  24516  fprodadd  24518  fprodneg  24544  fprodsub  24545  caytr  24566  osneisi  24697  0alg  24922  catsbc  25015  tareltsuc  25064  prismorcsetlem  25078  prismorcset  25080  segline  25307  bsstrs  25312  segray  25321  rayline  25322  ivthALT  25424  fness  25448  ssref  25449  fneref  25450  refref  25451  refssfne  25460  fnemeet1  25481  fnejoin2  25484  filnetlem2  25494  filnetlem4  25496  welb  25583  caures  25642  constcncf  25644  addccncf  25645  idcncf  25646  sub1cncf  25647  sub2cncf  25648  cnresima  25650  rngoidl  25815  ralxpmap  25927  lcomfsup  25934  ismrcd1  25939  ismrc  25942  incssnn0  25952  mzpclall  25971  rmydioph  26273  rmxdioph  26275  expdiophlem2  26281  expdioph  26282  aomclem6  26322  kelac1  26327  frlmsslsp  26414  frlmlbs  26415  frlmup1  26416  gicabl  26429  rgspnid  26543  symggen  26577  lhe4.4ex1a  26712  dvsconst  26713  dvsid  26714  dvsef  26715  dvconstbi  26717  onfrALTlem3  27002  onfrALTlem3VD  27353  bnj1253  27736  atpsubN  28743  pol1N  28900  1psubclN  28934  cdlemefrs32fva  29390  dia2dimlem13  30067  dibord  30150  dochvalr  30348  hdmapevec  30829
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator