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

Theorem ssid 3303
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 3288 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1717    C_ wss 3256
This theorem is referenced by:  eqimssi  3338  eqimss2i  3339  nsspssun  3510  inv1  3590  disjpss  3614  difid  3632  pwidg  3747  elssuni  3978  unimax  3984  intmin  4005  rintn0  4115  ordunidif  4563  iunpw  4692  onsucuni  4741  tfisi  4771  xpss1  4917  xpss2  4918  residm  5110  resdm  5117  resmpt3  5125  ssrnres  5242  dffn3  5531  fimacnv  5794  fparlem3  6380  fparlem4  6381  tfrlem1  6565  tz7.48-2  6628  abianfp  6645  oaordi  6718  omwordi  6743  omass  6752  nnaordi  6790  nnmwordi  6807  fpmg  6968  boxcutc  7034  domss2  7195  0fin  7265  en1eqsn  7267  fimax2g  7282  domunfican  7308  pwfi  7330  fissuni  7339  fipreima  7340  wofib  7440  wemapso  7446  sucprcreg  7493  noinfep  7540  noinfepOLD  7541  cantnfval2  7550  cantnfp1lem3  7562  tcidm  7611  tc0  7612  r1rankidb  7656  r1pw  7697  rankr1id  7714  scott0  7736  htalem  7746  xpomen  7823  infpwfien  7869  alephsmo  7909  dfac12lem3  7951  ackbij2lem4  8048  cflem  8052  cflecard  8059  cflim2  8069  cfslb  8072  fin4en1  8115  fin23lem13  8138  fin23lem15  8140  fin23lem36  8154  isf32lem1  8159  fin67  8201  dcomex  8253  zorn2lem4  8305  alephexp2  8382  fpwwe2lem13  8443  canthnumlem  8449  wunex2  8539  wuncidm  8547  eltsk2g  8552  axgroth6  8629  axgroth3  8632  xrsup  11169  expcl  11319  hashcard  11558  hashf1lem2  11625  lo1eq  12282  rlimeq  12283  serclim0  12291  isercolllem2  12379  isercoll  12381  summolem3  12428  isum  12433  fsumser  12444  fsumcl  12447  fsum2d  12475  fsumabs  12500  fsumrlim  12510  fsumo1  12511  fsumiun  12520  flo1  12554  eflt  12638  xpnnenOLD  12729  rpnnen2lem3  12736  rpnnen2lem5  12738  rpnnen2lem11  12744  rpnnen2  12745  rexpen  12747  eulerthlem2  13091  ressid  13444  ressinbas  13445  mremre  13749  yon11  14281  yon12  14282  yon2  14283  yonpropd  14285  oppcyon  14286  yonffth  14301  p0le  14392  ple1  14393  oduclatb  14491  ipopos  14506  fpwipodrs  14510  submid  14671  mulgnncl  14825  mulgnn0cl  14826  mulgcl  14827  subgid  14866  cntrnsg  15060  sylow3lem5  15185  lsmss1  15218  lsmss2  15220  gsumzres  15437  gsumzcl  15438  gsumzf1o  15439  gsumadd  15448  gsumzsplit  15449  gsumzmhm  15453  gsumzoppg  15459  gsumzinv  15460  gsumsub  15462  gsum2d  15466  dprdfinv  15497  dprdf1  15511  dmdprdsplitlem  15515  dprd2db  15521  dpjidcl  15536  ablfac1eulem  15550  ablfac1eu  15551  ablfaclem2  15564  gsumdixp  15635  subrgid  15790  lss1  15935  lbsextlem1  16150  rlmbas  16187  rlmplusg  16188  rlm0  16189  rlmmulr  16190  rlmsca  16191  rlmsca2  16192  rlmvsca  16193  rlmtopn  16194  rlmds  16195  psrass1lem  16362  mplsubglem  16418  mpllsslem  16419  mplsubrglem  16422  mplcoe1  16448  mplbas2  16451  evlslem4  16484  psrbagev1  16486  evlslem2  16488  znf1o  16748  zntoslem  16753  css0  16832  topopn  16895  fiinbas  16933  topbas  16953  topcld  17015  clstop  17049  ntrtop  17050  opnneissb  17094  opnssneib  17095  opnneiid  17106  neiptopuni  17110  neiptoptop  17111  maxlp  17126  isperf2  17131  restopn2  17156  restperf  17163  idcn  17236  cnconst2  17262  lmres  17279  rncmp  17374  fiuncmp  17382  cmpfi  17386  concn  17403  1stcelcls  17438  llyidm  17465  nllyidm  17466  toplly  17467  kgentopon  17484  kgencn2  17503  ptpjpre1  17517  ptbasfi  17527  ptcld  17559  xkopt  17601  elqtop2  17647  qtopuni  17648  ptcmpfi  17759  fbssfi  17783  opnfbas  17788  filtop  17801  isfil2  17802  isfild  17804  fsubbas  17813  ssfg  17818  filssufilg  17857  ufileu  17865  imaelfm  17897  rnelfm  17899  fmfnfmlem4  17903  neiflim  17920  supnfcls  17966  fclscf  17971  flimfnfcls  17974  tsmsfbas  18071  utopbas  18179  xpsxmet  18311  xpsdsval  18312  xpsmet  18313  tmsxms  18399  tmsms  18400  imasf1oxms  18402  imasf1oms  18403  prdsxms  18443  prdsms  18444  tmsxpsval  18451  retopbas  18658  cnngp  18678  cnperf  18715  retopcon  18724  fsumcn  18764  abscncf  18795  recncf  18796  imcncf  18797  cjcncf  18798  mulc1cncf  18799  cncfcn1  18804  cncfmpt2f  18808  cncfmpt2ss  18809  addccncf  18810  cdivcncf  18811  negcncf  18812  negfcncf  18813  abscncfALT  18814  cnmpt2pc  18817  xrhmeo  18835  oprpiece1res1  18840  oprpiece1res2  18841  cnrehmeo  18842  iscau3  19095  caubl  19124  caublcls  19125  evthicc2  19217  ovolre  19281  volsuplem  19309  uniiccdif  19330  uniioovol  19331  uniiccvol  19332  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  dyadmbllem  19351  volcn  19358  volivth  19359  itgfsum  19578  iblabslem  19579  iblabs  19580  bddmulibl  19590  cnlimc  19635  cnlimci  19636  dvres3  19660  dvres3a  19661  dvidlem  19662  dvcnp2  19666  dvcn  19667  dvnadd  19675  dvnres  19677  cpnord  19681  cpnres  19683  dvaddbr  19684  dvmulbr  19685  dvcmul  19690  dvcmulf  19691  dvcobr  19692  dvcjbr  19695  dvrec  19701  dvmptntr  19717  dvmptfsum  19719  dveflem  19723  dvef  19724  rolle  19734  dvlipcn  19738  c1liplem1  19740  dvgt0lem2  19747  dvivth  19754  lhop1lem  19757  dvfsumabs  19767  ftc1a  19781  ftc1cn  19787  ftc2  19788  deg1mul3le  19899  plyssc  19979  plyeq0  19990  coeeulem  20003  0dgr  20024  coemulc  20033  coe0  20034  coesub  20035  coe1termlem  20036  dgrmulc  20049  dgrsub  20050  dgrcolem1  20051  dgrcolem2  20052  dvnply2  20064  plycpn  20066  plyremlem  20081  fta1lem  20084  vieta1lem2  20088  aalioulem3  20111  dvntaylp  20147  taylthlem1  20149  taylthlem2  20150  ulmcn  20175  psercn  20202  pserdv  20205  abelth  20217  efcn  20219  efcvx  20225  pige3  20285  dvrelog  20388  logcn  20398  dvloglem  20399  dvlog  20402  dvlog2  20404  efopnlem2  20408  logccv  20414  cxpcn  20489  cxpcn2  20490  cxpcn3  20492  resqrcn  20493  sqrcn  20494  loglesqr  20502  atancn  20636  rlimcnp3  20666  jensen  20687  ftalem3  20717  basellem2  20724  dchrfi  20899  dchrisumlema  21042  pntrsumo1  21119  pntrsumbnd  21120  pntlem3  21163  cusgrasizeindslem2  21342  efghgrp  21802  sspid  22065  ssps  22070  helch  22587  hhssnv  22605  hhsssh  22610  shintcl  22673  chintcl  22675  shlesb1i  22729  omlsi  22747  chlejb1i  22819  chm0i  22833  chabs1  22859  chabs2  22860  spanun  22888  cmidi  22953  pjidmcoi  23521  csmdsymi  23678  sumdmdlem2  23763  dmdbr5ati  23766  mdcompli  23773  dmdcompli  23774  disjdifprg  23854  fdmrn  23875  xppreima  23894  xrsmulgzz  24026  pnfneige0  24133  esumsn  24245  esumcvg  24265  pwsiga  24302  sigagenid  24323  lgamgulmlem2  24586  cvmlift2lem6  24767  relexpdm  24907  relexprn  24908  rtrclreclem.refl  24916  rtrclreclem.subset  24917  prodmolem3  25031  iprod  25036  iprodn0  25038  fprodss  25046  fprodcl  25050  risefaccl  25092  fallfaccl  25093  trpredtr  25250  trpredpo  25255  frrlem5c  25304  frrlem10  25309  ontgval  25888  ovoliunnfl  25946  voliunnfl  25948  volsupnfl  25949  ftc1cnnclem  25971  ftc1cnnc  25972  areacirclem3  25976  areacirclem4  25977  areacirclem1  25978  areacirclem5  25979  ivthALT  26022  fness  26046  ssref  26047  fneref  26048  refref  26049  refssfne  26058  fnemeet1  26079  fnejoin2  26082  filnetlem2  26092  filnetlem4  26094  welb  26122  caures  26150  constcncf  26152  idcncf  26153  sub1cncf  26154  sub2cncf  26155  cnresima  26157  rngoidl  26318  ralxpmap  26426  lcomfsup  26431  ismrcd1  26436  ismrc  26439  incssnn0  26449  mzpclall  26468  rmydioph  26769  rmxdioph  26771  expdiophlem2  26777  expdioph  26778  aomclem6  26818  kelac1  26823  frlmsslsp  26910  frlmlbs  26911  frlmup1  26912  gicabl  26925  rgspnid  27039  symggen  27073  lhe4.4ex1a  27208  dvsconst  27209  dvsid  27210  dvsef  27211  dvconstbi  27213  dvcosre  27402  itgsinexplem1  27409  funresfunco  27651  onfrALTlem3  27966  onfrALTlem3VD  28333  bnj1253  28717  atpsubN  29918  pol1N  30075  1psubclN  30109  cdlemefrs32fva  30565  dia2dimlem13  31242  dibord  31325  dochvalr  31523  hdmapevec  32004
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator