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

Theorem ssid 3331
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 3316 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    C_ wss 3284
This theorem is referenced by:  eqimssi  3366  eqimss2i  3367  nsspssun  3538  inv1  3618  disjpss  3642  difid  3660  pwidg  3775  elssuni  4007  unimax  4013  intmin  4034  rintn0  4145  ordunidif  4593  iunpw  4722  onsucuni  4771  tfisi  4801  xpss1  4947  xpss2  4948  residm  5140  resdm  5147  resmpt3  5155  ssrnres  5272  dffn3  5561  fimacnv  5825  fparlem3  6411  fparlem4  6412  tfrlem1  6599  tz7.48-2  6662  abianfp  6679  oaordi  6752  omwordi  6777  omass  6786  nnaordi  6824  nnmwordi  6841  fpmg  7002  boxcutc  7068  domss2  7229  0fin  7299  en1eqsn  7301  fimax2g  7316  domunfican  7342  pwfi  7364  fissuni  7373  fipreima  7374  wofib  7474  wemapso  7480  sucprcreg  7527  noinfep  7574  noinfepOLD  7575  cantnfval2  7584  cantnfp1lem3  7596  tcidm  7645  tc0  7646  r1rankidb  7690  r1pw  7731  rankr1id  7748  scott0  7770  htalem  7780  xpomen  7857  infpwfien  7903  alephsmo  7943  dfac12lem3  7985  ackbij2lem4  8082  cflem  8086  cflecard  8093  cflim2  8103  cfslb  8106  fin4en1  8149  fin23lem13  8172  fin23lem15  8174  fin23lem36  8188  isf32lem1  8193  fin67  8235  dcomex  8287  zorn2lem4  8339  alephexp2  8416  fpwwe2lem13  8477  canthnumlem  8483  wunex2  8573  wuncidm  8581  eltsk2g  8586  axgroth6  8663  axgroth3  8666  xrsup  11208  expcl  11358  hashcard  11597  hashf1lem2  11664  lo1eq  12321  rlimeq  12322  serclim0  12330  isercolllem2  12418  isercoll  12420  summolem3  12467  isum  12472  fsumser  12483  fsumcl  12486  fsum2d  12514  fsumabs  12539  fsumrlim  12549  fsumo1  12550  fsumiun  12559  flo1  12593  eflt  12677  xpnnenOLD  12768  rpnnen2lem3  12775  rpnnen2lem5  12777  rpnnen2lem11  12783  rpnnen2  12784  rexpen  12786  eulerthlem2  13130  ressid  13483  ressinbas  13484  mremre  13788  yon11  14320  yon12  14321  yon2  14322  yonpropd  14324  oppcyon  14325  yonffth  14340  p0le  14431  ple1  14432  oduclatb  14530  ipopos  14545  fpwipodrs  14549  submid  14710  mulgnncl  14864  mulgnn0cl  14865  mulgcl  14866  subgid  14905  cntrnsg  15099  sylow3lem5  15224  lsmss1  15257  lsmss2  15259  gsumzres  15476  gsumzcl  15477  gsumzf1o  15478  gsumadd  15487  gsumzsplit  15488  gsumzmhm  15492  gsumzoppg  15498  gsumzinv  15499  gsumsub  15501  gsum2d  15505  dprdfinv  15536  dprdf1  15550  dmdprdsplitlem  15554  dprd2db  15560  dpjidcl  15575  ablfac1eulem  15589  ablfac1eu  15590  ablfaclem2  15603  gsumdixp  15674  subrgid  15829  lss1  15974  lbsextlem1  16189  rlmbas  16226  rlmplusg  16227  rlm0  16228  rlmmulr  16229  rlmsca  16230  rlmsca2  16231  rlmvsca  16232  rlmtopn  16233  rlmds  16234  psrass1lem  16401  mplsubglem  16457  mpllsslem  16458  mplsubrglem  16461  mplcoe1  16487  mplbas2  16490  evlslem4  16523  psrbagev1  16525  evlslem2  16527  znf1o  16791  zntoslem  16796  css0  16875  topopn  16938  fiinbas  16976  topbas  16996  topcld  17058  clstop  17092  ntrtop  17093  opnneissb  17137  opnssneib  17138  opnneiid  17149  neiptopuni  17153  neiptoptop  17154  maxlp  17169  isperf2  17174  restopn2  17199  restperf  17206  idcn  17279  cnconst2  17305  lmres  17322  rncmp  17417  fiuncmp  17425  cmpfi  17429  concn  17446  1stcelcls  17481  llyidm  17508  nllyidm  17509  toplly  17510  kgentopon  17527  kgencn2  17546  ptpjpre1  17560  ptbasfi  17570  ptcld  17602  xkopt  17644  elqtop2  17690  qtopuni  17691  ptcmpfi  17802  fbssfi  17826  opnfbas  17831  filtop  17844  isfil2  17845  isfild  17847  fsubbas  17856  ssfg  17861  filssufilg  17900  ufileu  17908  imaelfm  17940  rnelfm  17942  fmfnfmlem4  17946  neiflim  17963  supnfcls  18009  fclscf  18014  flimfnfcls  18017  tsmsfbas  18114  utopbas  18222  xpsxmet  18367  xpsdsval  18368  xpsmet  18369  tmsxms  18473  tmsms  18474  imasf1oxms  18476  imasf1oms  18477  prdsxms  18517  prdsms  18518  tmsxpsval  18525  retopbas  18751  cnngp  18771  cnperf  18808  retopcon  18817  fsumcn  18857  abscncf  18888  recncf  18889  imcncf  18890  cjcncf  18891  mulc1cncf  18892  cncfcn1  18897  cncfmpt2f  18901  cncfmpt2ss  18902  addccncf  18903  cdivcncf  18904  negcncf  18905  negfcncf  18906  abscncfALT  18907  cnmpt2pc  18910  xrhmeo  18928  oprpiece1res1  18933  oprpiece1res2  18934  cnrehmeo  18935  iscau3  19188  caubl  19217  caublcls  19218  evthicc2  19314  ovolre  19378  volsuplem  19406  uniiccdif  19427  uniioovol  19428  uniiccvol  19429  uniioombllem3  19434  uniioombllem4  19435  uniioombllem5  19436  dyadmbllem  19448  volcn  19455  volivth  19456  itgfsum  19675  iblabslem  19676  iblabs  19677  bddmulibl  19687  cnlimc  19732  cnlimci  19733  dvres3  19757  dvres3a  19758  dvidlem  19759  dvcnp2  19763  dvcn  19764  dvnadd  19772  dvnres  19774  cpnord  19778  cpnres  19780  dvaddbr  19781  dvmulbr  19782  dvcmul  19787  dvcmulf  19788  dvcobr  19789  dvcjbr  19792  dvrec  19798  dvmptntr  19814  dvmptfsum  19816  dveflem  19820  dvef  19821  rolle  19831  dvlipcn  19835  c1liplem1  19837  dvgt0lem2  19844  dvivth  19851  lhop1lem  19854  dvfsumabs  19864  ftc1a  19878  ftc1cn  19884  ftc2  19885  deg1mul3le  19996  plyssc  20076  plyeq0  20087  coeeulem  20100  0dgr  20121  coemulc  20130  coe0  20131  coesub  20132  coe1termlem  20133  dgrmulc  20146  dgrsub  20147  dgrcolem1  20148  dgrcolem2  20149  dvnply2  20161  plycpn  20163  plyremlem  20178  fta1lem  20181  vieta1lem2  20185  aalioulem3  20208  dvntaylp  20244  taylthlem1  20246  taylthlem2  20247  ulmcn  20272  psercn  20299  pserdv  20302  abelth  20314  efcn  20316  efcvx  20322  pige3  20382  dvrelog  20485  logcn  20495  dvloglem  20496  dvlog  20499  dvlog2  20501  efopnlem2  20505  logccv  20511  cxpcn  20586  cxpcn2  20587  cxpcn3  20589  resqrcn  20590  sqrcn  20591  loglesqr  20599  atancn  20733  rlimcnp3  20763  jensen  20784  ftalem3  20814  basellem2  20821  dchrfi  20996  dchrisumlema  21139  pntrsumo1  21216  pntrsumbnd  21217  pntlem3  21260  cusgrasizeindslem2  21440  efghgrp  21918  sspid  22181  ssps  22186  helch  22703  hhssnv  22721  hhsssh  22726  shintcl  22789  chintcl  22791  shlesb1i  22845  omlsi  22863  chlejb1i  22935  chm0i  22949  chabs1  22975  chabs2  22976  spanun  23004  cmidi  23069  pjidmcoi  23637  csmdsymi  23794  sumdmdlem2  23879  dmdbr5ati  23882  mdcompli  23889  dmdcompli  23890  disjdifprg  23974  fdmrn  23996  xppreima  24016  xrinfm  24078  clatp0ex  24150  clatp1ex  24151  xrsmulgzz  24157  xrsp0  24160  xrsp1  24161  pnfneige0  24293  esumsn  24413  esumcvg  24433  pwsiga  24470  sigagenid  24491  lgamgulmlem2  24771  cvmlift2lem6  24952  relexpdm  25092  relexprn  25093  rtrclreclem.refl  25101  rtrclreclem.subset  25102  prodmolem3  25216  iprod  25221  iprodn0  25223  fprodss  25231  fprodcl  25235  fprod2d  25262  risefaccl  25287  fallfaccl  25288  trpredtr  25451  trpredpo  25456  frrlem5c  25505  frrlem10  25510  ontgval  26089  mblfinlem2  26148  mblfinlem3  26149  ismblfin  26150  ovoliunnfl  26151  voliunnfl  26153  volsupnfl  26154  mbfposadd  26157  ftc1cnnclem  26181  ftc1cnnc  26182  areacirclem3  26186  areacirclem4  26187  areacirclem1  26188  areacirclem5  26189  ivthALT  26232  fness  26256  ssref  26257  fneref  26258  refref  26259  refssfne  26268  fnemeet1  26289  fnejoin2  26292  filnetlem2  26302  filnetlem4  26304  welb  26332  caures  26360  constcncf  26362  idcncf  26363  sub1cncf  26364  sub2cncf  26365  cnresima  26367  rngoidl  26528  ralxpmap  26636  lcomfsup  26641  ismrcd1  26646  ismrc  26649  incssnn0  26659  mzpclall  26678  rmydioph  26979  rmxdioph  26981  expdiophlem2  26987  expdioph  26988  aomclem6  27028  kelac1  27033  frlmsslsp  27120  frlmlbs  27121  frlmup1  27122  gicabl  27135  rgspnid  27249  symggen  27283  lhe4.4ex1a  27418  dvsconst  27419  dvsid  27420  dvsef  27421  dvconstbi  27423  dvcosre  27612  itgsinexplem1  27619  funresfunco  27860  onfrALTlem3  28345  onfrALTlem3VD  28712  bnj1253  29096  atpsubN  30239  pol1N  30396  1psubclN  30430  cdlemefrs32fva  30886  dia2dimlem13  31563  dibord  31646  dochvalr  31844  hdmapevec  32325
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 2389
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 2395  df-cleq 2401  df-clel 2404  df-in 3291  df-ss 3298
  Copyright terms: Public domain W3C validator