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

Theorem ssid 3327
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 3312 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    C_ wss 3280
This theorem is referenced by:  eqimssi  3362  eqimss2i  3363  nsspssun  3534  inv1  3614  disjpss  3638  difid  3656  pwidg  3771  elssuni  4003  unimax  4009  intmin  4030  rintn0  4141  ordunidif  4589  iunpw  4718  onsucuni  4767  tfisi  4797  xpss1  4943  xpss2  4944  residm  5136  resdm  5143  resmpt3  5151  ssrnres  5268  dffn3  5557  fimacnv  5821  fparlem3  6407  fparlem4  6408  tfrlem1  6595  tz7.48-2  6658  abianfp  6675  oaordi  6748  omwordi  6773  omass  6782  nnaordi  6820  nnmwordi  6837  fpmg  6998  boxcutc  7064  domss2  7225  0fin  7295  en1eqsn  7297  fimax2g  7312  domunfican  7338  pwfi  7360  fissuni  7369  fipreima  7370  wofib  7470  wemapso  7476  sucprcreg  7523  noinfep  7570  noinfepOLD  7571  cantnfval2  7580  cantnfp1lem3  7592  tcidm  7641  tc0  7642  r1rankidb  7686  r1pw  7727  rankr1id  7744  scott0  7766  htalem  7776  xpomen  7853  infpwfien  7899  alephsmo  7939  dfac12lem3  7981  ackbij2lem4  8078  cflem  8082  cflecard  8089  cflim2  8099  cfslb  8102  fin4en1  8145  fin23lem13  8168  fin23lem15  8170  fin23lem36  8184  isf32lem1  8189  fin67  8231  dcomex  8283  zorn2lem4  8335  alephexp2  8412  fpwwe2lem13  8473  canthnumlem  8479  wunex2  8569  wuncidm  8577  eltsk2g  8582  axgroth6  8659  axgroth3  8662  xrsup  11204  expcl  11354  hashcard  11593  hashf1lem2  11660  lo1eq  12317  rlimeq  12318  serclim0  12326  isercolllem2  12414  isercoll  12416  summolem3  12463  isum  12468  fsumser  12479  fsumcl  12482  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  flo1  12589  eflt  12673  xpnnenOLD  12764  rpnnen2lem3  12771  rpnnen2lem5  12773  rpnnen2lem11  12779  rpnnen2  12780  rexpen  12782  eulerthlem2  13126  ressid  13479  ressinbas  13480  mremre  13784  yon11  14316  yon12  14317  yon2  14318  yonpropd  14320  oppcyon  14321  yonffth  14336  p0le  14427  ple1  14428  oduclatb  14526  ipopos  14541  fpwipodrs  14545  submid  14706  mulgnncl  14860  mulgnn0cl  14861  mulgcl  14862  subgid  14901  cntrnsg  15095  sylow3lem5  15220  lsmss1  15253  lsmss2  15255  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumadd  15483  gsumzsplit  15484  gsumzmhm  15488  gsumzoppg  15494  gsumzinv  15495  gsumsub  15497  gsum2d  15501  dprdfinv  15532  dprdf1  15546  dmdprdsplitlem  15550  dprd2db  15556  dpjidcl  15571  ablfac1eulem  15585  ablfac1eu  15586  ablfaclem2  15599  gsumdixp  15670  subrgid  15825  lss1  15970  lbsextlem1  16185  rlmbas  16222  rlmplusg  16223  rlm0  16224  rlmmulr  16225  rlmsca  16226  rlmsca2  16227  rlmvsca  16228  rlmtopn  16229  rlmds  16230  psrass1lem  16397  mplsubglem  16453  mpllsslem  16454  mplsubrglem  16457  mplcoe1  16483  mplbas2  16486  evlslem4  16519  psrbagev1  16521  evlslem2  16523  znf1o  16787  zntoslem  16792  css0  16871  topopn  16934  fiinbas  16972  topbas  16992  topcld  17054  clstop  17088  ntrtop  17089  opnneissb  17133  opnssneib  17134  opnneiid  17145  neiptopuni  17149  neiptoptop  17150  maxlp  17165  isperf2  17170  restopn2  17195  restperf  17202  idcn  17275  cnconst2  17301  lmres  17318  rncmp  17413  fiuncmp  17421  cmpfi  17425  concn  17442  1stcelcls  17477  llyidm  17504  nllyidm  17505  toplly  17506  kgentopon  17523  kgencn2  17542  ptpjpre1  17556  ptbasfi  17566  ptcld  17598  xkopt  17640  elqtop2  17686  qtopuni  17687  ptcmpfi  17798  fbssfi  17822  opnfbas  17827  filtop  17840  isfil2  17841  isfild  17843  fsubbas  17852  ssfg  17857  filssufilg  17896  ufileu  17904  imaelfm  17936  rnelfm  17938  fmfnfmlem4  17942  neiflim  17959  supnfcls  18005  fclscf  18010  flimfnfcls  18013  tsmsfbas  18110  utopbas  18218  xpsxmet  18363  xpsdsval  18364  xpsmet  18365  tmsxms  18469  tmsms  18470  imasf1oxms  18472  imasf1oms  18473  prdsxms  18513  prdsms  18514  tmsxpsval  18521  retopbas  18747  cnngp  18767  cnperf  18804  retopcon  18813  fsumcn  18853  abscncf  18884  recncf  18885  imcncf  18886  cjcncf  18887  mulc1cncf  18888  cncfcn1  18893  cncfmpt2f  18897  cncfmpt2ss  18898  addccncf  18899  cdivcncf  18900  negcncf  18901  negfcncf  18902  abscncfALT  18903  cnmpt2pc  18906  xrhmeo  18924  oprpiece1res1  18929  oprpiece1res2  18930  cnrehmeo  18931  iscau3  19184  caubl  19213  caublcls  19214  evthicc2  19310  ovolre  19374  volsuplem  19402  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  dyadmbllem  19444  volcn  19451  volivth  19452  itgfsum  19671  iblabslem  19672  iblabs  19673  bddmulibl  19683  cnlimc  19728  cnlimci  19729  dvres3  19753  dvres3a  19754  dvidlem  19755  dvcnp2  19759  dvcn  19760  dvnadd  19768  dvnres  19770  cpnord  19774  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvcmul  19783  dvcmulf  19784  dvcobr  19785  dvcjbr  19788  dvrec  19794  dvmptntr  19810  dvmptfsum  19812  dveflem  19816  dvef  19817  rolle  19827  dvlipcn  19831  c1liplem1  19833  dvgt0lem2  19840  dvivth  19847  lhop1lem  19850  dvfsumabs  19860  ftc1a  19874  ftc1cn  19880  ftc2  19881  deg1mul3le  19992  plyssc  20072  plyeq0  20083  coeeulem  20096  0dgr  20117  coemulc  20126  coe0  20127  coesub  20128  coe1termlem  20129  dgrmulc  20142  dgrsub  20143  dgrcolem1  20144  dgrcolem2  20145  dvnply2  20157  plycpn  20159  plyremlem  20174  fta1lem  20177  vieta1lem2  20181  aalioulem3  20204  dvntaylp  20240  taylthlem1  20242  taylthlem2  20243  ulmcn  20268  psercn  20295  pserdv  20298  abelth  20310  efcn  20312  efcvx  20318  pige3  20378  dvrelog  20481  logcn  20491  dvloglem  20492  dvlog  20495  dvlog2  20497  efopnlem2  20501  logccv  20507  cxpcn  20582  cxpcn2  20583  cxpcn3  20585  resqrcn  20586  sqrcn  20587  loglesqr  20595  atancn  20729  rlimcnp3  20759  jensen  20780  ftalem3  20810  basellem2  20817  dchrfi  20992  dchrisumlema  21135  pntrsumo1  21212  pntrsumbnd  21213  pntlem3  21256  cusgrasizeindslem2  21436  efghgrp  21914  sspid  22177  ssps  22182  helch  22699  hhssnv  22717  hhsssh  22722  shintcl  22785  chintcl  22787  shlesb1i  22841  omlsi  22859  chlejb1i  22931  chm0i  22945  chabs1  22971  chabs2  22972  spanun  23000  cmidi  23065  pjidmcoi  23633  csmdsymi  23790  sumdmdlem2  23875  dmdbr5ati  23878  mdcompli  23885  dmdcompli  23886  disjdifprg  23970  fdmrn  23992  xppreima  24012  xrinfm  24074  clatp0ex  24146  clatp1ex  24147  xrsmulgzz  24153  xrsp0  24156  xrsp1  24157  pnfneige0  24289  esumsn  24409  esumcvg  24429  pwsiga  24466  sigagenid  24487  lgamgulmlem2  24767  cvmlift2lem6  24948  relexpdm  25088  relexprn  25089  rtrclreclem.refl  25097  rtrclreclem.subset  25098  prodmolem3  25212  iprod  25217  iprodn0  25219  fprodss  25227  fprodcl  25231  fprod2d  25258  risefaccl  25283  fallfaccl  25284  trpredtr  25447  trpredpo  25452  frrlem5c  25501  frrlem10  25506  ontgval  26085  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfposadd  26153  ftc1cnnclem  26177  ftc1cnnc  26178  areacirclem3  26182  areacirclem4  26183  areacirclem1  26184  areacirclem5  26185  ivthALT  26228  fness  26252  ssref  26253  fneref  26254  refref  26255  refssfne  26264  fnemeet1  26285  fnejoin2  26288  filnetlem2  26298  filnetlem4  26300  welb  26328  caures  26356  constcncf  26358  idcncf  26359  sub1cncf  26360  sub2cncf  26361  cnresima  26363  rngoidl  26524  ralxpmap  26632  lcomfsup  26637  ismrcd1  26642  ismrc  26645  incssnn0  26655  mzpclall  26674  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  aomclem6  27024  kelac1  27029  frlmsslsp  27116  frlmlbs  27117  frlmup1  27118  gicabl  27131  rgspnid  27245  symggen  27279  lhe4.4ex1a  27414  dvsconst  27415  dvsid  27416  dvsef  27417  dvconstbi  27419  dvcosre  27608  itgsinexplem1  27615  funresfunco  27856  onfrALTlem3  28341  onfrALTlem3VD  28708  bnj1253  29092  atpsubN  30235  pol1N  30392  1psubclN  30426  cdlemefrs32fva  30882  dia2dimlem13  31559  dibord  31642  dochvalr  31840  hdmapevec  32321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator