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

Theorem ssid 3139
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 3126 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3094
This theorem is referenced by:  eqimssi  3174  eqimss2i  3175  nsspssun  3344  inv1  3423  disjpss  3447  difid  3464  pwidg  3578  elssuni  3796  unimax  3802  intmin  3823  rintn0  3933  ordunidif  4377  iunpw  4507  onsucuni  4556  tfisi  4586  xpss1  4748  xpss2  4749  residm  4939  resdm  4946  resmpt3  4954  ssrnres  5069  dffn3  5299  fimacnv  5556  fparlem3  6119  fparlem4  6120  tfrlem1  6324  tz7.48-2  6387  abianfp  6404  oaordi  6477  omwordi  6502  omass  6511  nnaordi  6549  nnmwordi  6566  fpmg  6726  boxcutc  6792  domss2  6953  0fin  7020  en1eqsn  7021  fimax2g  7036  domunfican  7062  pwfi  7084  fissuni  7093  fipreima  7094  wofib  7193  wemapso  7199  sucprcreg  7246  noinfep  7293  noinfepOLD  7294  cantnfval2  7303  cantnfp1lem3  7315  tcidm  7364  tc0  7365  r1rankidb  7409  r1pw  7450  rankr1id  7467  scott0  7489  htalem  7499  xpomen  7576  infpwfien  7622  alephsmo  7662  dfac12lem3  7704  ackbij2lem4  7801  cflem  7805  cflecard  7812  cflim2  7822  cfslb  7825  fin4en1  7868  fin23lem13  7891  fin23lem15  7893  fin23lem36  7907  isf32lem1  7912  fin67  7954  dcomex  8006  zorn2lem4  8059  alephexp2  8136  fpwwe2lem13  8197  canthnumlem  8203  wunex2  8293  wuncidm  8301  eltsk2g  8306  axgroth6  8383  axgroth3  8386  xrsup  10903  expcl  11052  hashcard  11280  hashf1lem2  11324  lo1eq  11972  rlimeq  11973  serclim0  11981  isercolllem2  12069  isercoll  12071  summolem3  12117  isum  12122  fsumser  12133  fsumcl  12136  fsum2d  12164  fsumabs  12189  fsumrlim  12199  fsumo1  12200  fsumiun  12209  flo1  12240  eflt  12324  xpnnenOLD  12415  rpnnen2lem3  12422  rpnnen2lem5  12424  rpnnen2lem11  12430  rpnnen2  12431  rexpen  12433  eulerthlem2  12777  ressid  13130  ressinbas  13131  mremre  13433  yon11  13965  yon12  13966  yon2  13967  yonpropd  13969  oppcyon  13970  yonffth  13985  p0le  14076  ple1  14077  oduclatb  14175  ipopos  14190  fpwipodrs  14194  submid  14355  mulgnncl  14509  mulgnn0cl  14510  mulgcl  14511  subgid  14550  cntrnsg  14744  sylow3lem5  14869  lsmss1  14902  lsmss2  14904  gsumzres  15121  gsumzcl  15122  gsumzf1o  15123  gsumadd  15132  gsumzsplit  15133  gsumzmhm  15137  gsumzoppg  15143  gsumzinv  15144  gsumsub  15146  gsum2d  15150  dprdfinv  15181  dprdf1  15195  dmdprdsplitlem  15199  dprd2db  15205  dpjidcl  15220  ablfac1eulem  15234  ablfac1eu  15235  ablfaclem2  15248  gsumdixp  15319  subrgid  15474  lss1  15623  lbsextlem1  15838  rlmbas  15875  rlmplusg  15876  rlm0  15877  rlmmulr  15878  rlmsca  15879  rlmsca2  15880  rlmvsca  15881  rlmtopn  15882  rlmds  15883  psrass1lem  16050  mplsubglem  16106  mpllsslem  16107  mplsubrglem  16110  mplcoe1  16136  mplbas2  16139  evlslem4  16172  psrbagev1  16174  evlslem2  16176  znf1o  16432  zntoslem  16437  css0  16516  topopn  16579  fiinbas  16617  topbas  16637  topcld  16699  clstop  16733  ntrtop  16734  opnneissb  16778  opnssneib  16779  opnneiid  16790  maxlp  16805  isperf2  16810  restopn2  16835  restperf  16841  idcn  16914  cnconst2  16938  lmres  16955  rncmp  17050  fiuncmp  17058  cmpfi  17062  concn  17079  1stcelcls  17114  llyidm  17141  nllyidm  17142  toplly  17143  kgentopon  17160  kgencn2  17179  ptpjpre1  17193  ptbasfi  17203  ptcld  17234  xkopt  17276  elqtop2  17319  qtopuni  17320  ptcmpfi  17431  fbssfi  17459  opnfbas  17464  filtop  17477  isfil2  17478  isfild  17480  fsubbas  17489  ssfg  17494  filssufilg  17533  ufileu  17541  imaelfm  17573  rnelfm  17575  fmfnfmlem4  17579  neiflim  17596  supnfcls  17642  fclscf  17647  flimfnfcls  17650  tsmsfbas  17737  xpsxmet  17871  xpsdsval  17872  xpsmet  17873  tmsxms  17959  tmsms  17960  imasf1oxms  17962  imasf1oms  17963  prdsxms  18003  prdsms  18004  tmsxpsval  18011  retopbas  18196  cnngp  18216  cnperf  18252  retopcon  18261  fsumcn  18301  abscncf  18332  recncf  18333  imcncf  18334  cjcncf  18335  mulc1cncf  18336  cncfcn1  18341  cncfmpt2f  18345  cncfmpt2ss  18346  cdivcncf  18347  negcncf  18348  negfcncf  18349  abscncfALT  18350  cnmpt2pc  18353  xrhmeo  18371  oprpiece1res1  18376  oprpiece1res2  18377  cnrehmeo  18378  iscau3  18631  caubl  18660  caublcls  18661  evthicc2  18747  ovolre  18811  volsuplem  18839  uniiccdif  18860  uniioovol  18861  uniiccvol  18862  uniioombllem3  18867  uniioombllem4  18868  uniioombllem5  18869  dyadmbllem  18881  volcn  18888  volivth  18889  itgfsum  19108  iblabslem  19109  iblabs  19110  bddmulibl  19120  cnlimc  19165  cnlimci  19166  dvres3  19190  dvres3a  19191  dvidlem  19192  dvcnp2  19196  dvcn  19197  dvnadd  19205  dvnres  19207  cpnord  19211  cpnres  19213  dvaddbr  19214  dvmulbr  19215  dvcmul  19220  dvcmulf  19221  dvcobr  19222  dvcjbr  19225  dvrec  19231  dvmptntr  19247  dvmptfsum  19249  dveflem  19253  dvef  19254  rolle  19264  dvlipcn  19268  c1liplem1  19270  dvgt0lem2  19277  dvivth  19284  lhop1lem  19287  dvfsumabs  19297  ftc1a  19311  ftc1cn  19317  ftc2  19318  deg1mul3le  19429  plyssc  19509  plyeq0  19520  coeeulem  19533  0dgr  19554  coemulc  19563  coe0  19564  coesub  19565  coe1termlem  19566  dgrmulc  19579  dgrsub  19580  dgrcolem1  19581  dgrcolem2  19582  dvnply2  19594  plycpn  19596  plyremlem  19611  fta1lem  19614  vieta1lem2  19618  aalioulem3  19641  dvntaylp  19677  taylthlem1  19679  taylthlem2  19680  ulmcn  19703  psercn  19729  pserdv  19732  abelth  19744  efcn  19746  efcvx  19752  pige3  19812  dvrelog  19911  logcn  19921  dvloglem  19922  dvlog  19925  dvlog2  19927  efopnlem2  19931  logccv  19937  cxpcn  20012  cxpcn2  20013  cxpcn3  20015  resqrcn  20016  sqrcn  20017  loglesqr  20025  atancn  20159  rlimcnp3  20189  jensen  20210  ftalem3  20239  basellem2  20246  dchrfi  20421  dchrisumlema  20564  pntrsumo1  20641  pntrsumbnd  20642  pntlem3  20685  efghgrp  20965  sspid  21226  ssps  21231  helch  21748  hhssnv  21766  hhsssh  21771  shintcl  21834  chintcl  21836  shlesb1i  21890  omlsi  21908  chlejb1i  21980  chm0i  21994  chabs1  22020  chabs2  22021  spanun  22049  cmidi  22132  pjidmcoi  22682  csmdsymi  22839  sumdmdlem2  22924  dmdbr5ati  22927  mdcompli  22934  dmdcompli  22935  fdmrn  22961  cvmlift2lem6  23176  relexpdm  23369  relexprn  23370  rtrclreclem.refl  23378  rtrclreclem.subset  23379  trpredtr  23567  trpredpo  23572  frrlem5c  23621  frrlem10  23626  ontgval  24210  residcp  24408  prl2  24501  inpc  24609  inposet  24610  dominc  24612  rninc  24613  domncnt  24614  ranncnt  24615  dfps2  24621  toplat  24622  fsumprd  24661  clfsebs  24679  fincmpzer  24682  fprodadd  24684  fprodneg  24710  fprodsub  24711  caytr  24732  osneisi  24863  0alg  25088  catsbc  25181  tareltsuc  25230  prismorcsetlem  25244  prismorcset  25246  segline  25473  bsstrs  25478  segray  25487  rayline  25488  ivthALT  25590  fness  25614  ssref  25615  fneref  25616  refref  25617  refssfne  25626  fnemeet1  25647  fnejoin2  25650  filnetlem2  25660  filnetlem4  25662  welb  25749  caures  25808  constcncf  25810  addccncf  25811  idcncf  25812  sub1cncf  25813  sub2cncf  25814  cnresima  25816  rngoidl  25981  ralxpmap  26093  lcomfsup  26100  ismrcd1  26105  ismrc  26108  incssnn0  26118  mzpclall  26137  rmydioph  26439  rmxdioph  26441  expdiophlem2  26447  expdioph  26448  aomclem6  26488  kelac1  26493  frlmsslsp  26580  frlmlbs  26581  frlmup1  26582  gicabl  26595  rgspnid  26709  symggen  26743  lhe4.4ex1a  26878  dvsconst  26879  dvsid  26880  dvsef  26881  dvconstbi  26883  onfrALTlem3  27325  onfrALTlem3VD  27676  bnj1253  28059  atpsubN  29072  pol1N  29229  1psubclN  29263  cdlemefrs32fva  29719  dia2dimlem13  30396  dibord  30479  dochvalr  30677  hdmapevec  31158
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 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator