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

Theorem ssid 3370
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 21-Jun-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 22 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3355 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  eqimssi  3405  eqimss2i  3406  nsspssun  3578  inv1  3659  disjpss  3724  difid  3742  pwidg  3868  elssuni  4116  unimax  4122  intmin  4143  rintn0  4256  sseliALT  4418  ordunidif  4762  xpss1  4943  xpss2  4944  residm  5136  resdm  5143  resmpt3  5152  ssrnres  5271  dffn3  5561  fdmrn  5568  fvreseq1  5799  fimacnv  5830  iunpw  6385  onsucuni  6434  tfisi  6464  fparlem3  6669  fparlem4  6670  funsssuppss  6710  suppofss1d  6721  suppofss2d  6722  tfrlem1  6827  tz7.48-2  6889  oaordi  6977  omwordi  7002  omass  7011  nnaordi  7049  nnmwordi  7066  fpmg  7230  ralxpmap  7254  boxcutc  7298  domss2  7462  0fin  7532  en1eqsn  7534  findcard2d  7546  fimax2g  7550  domunfican  7576  pwfi  7598  fissuni  7608  fipreima  7609  fsuppmptif  7641  fsuppco2  7644  fsuppcor  7645  mapfienlem1  7646  mapfienlem2  7647  wofib  7751  wemapso  7757  sucprcregOLD  7807  noinfep  7857  noinfepOLD  7858  cantnfval2  7869  cantnfp1lem3  7880  cantnflem1d  7888  cantnflem1  7889  cantnfval2OLD  7899  cantnfp1lem3OLD  7906  tcidm  7958  tc0  7959  r1rankidb  8003  r1pw  8044  rankr1id  8061  scott0  8085  htalem  8095  xpomen  8174  infpwfien  8224  alephsmo  8264  dfac12lem3  8306  ackbij2lem4  8403  cflem  8407  cflecard  8414  cflim2  8424  cfslb  8427  fin4en1  8470  fin23lem13  8493  fin23lem15  8495  fin23lem36  8509  isf32lem1  8514  fin67  8556  dcomex  8608  zorn2lem4  8660  alephexp2  8737  fpwwe2lem13  8801  canthnumlem  8807  wunex2  8897  wuncidm  8905  eltsk2g  8910  axgroth6  8987  axgroth3  8990  xrsup  11699  expcl  11875  hashcard  12117  hashf1lem2  12201  lo1eq  13038  rlimeq  13039  serclim0  13047  isercolllem2  13135  isercoll  13137  summolem3  13183  isum  13188  fsumser  13199  fsumcl  13202  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  flo1  13309  eflt  13393  xpnnenOLD  13484  rpnnen2lem3  13491  rpnnen2lem5  13493  rpnnen2lem11  13499  rpnnen2  13500  rexpen  13502  eulerthlem2  13849  ressid  14225  ressinbas  14226  mremre  14534  yon11  15066  yon12  15067  yon2  15068  yonpropd  15070  oppcyon  15071  yonffth  15086  oduclatb  15306  ipopos  15322  fpwipodrs  15326  submid  15470  mulgnncl  15633  mulgnn0cl  15634  mulgcl  15635  subgid  15674  cntrnsg  15850  symggen  15967  sylow3lem5  16121  lsmss1  16154  lsmss2  16156  gsumzres  16379  gsumzcl2  16380  gsumzf1o  16382  gsumzresOLD  16383  gsumzclOLD  16384  gsumzf1oOLD  16385  gsumadd  16403  gsumaddOLD  16404  gsumzsplitOLD  16410  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  gsumzinvOLD  16433  gsumsubOLD  16438  gsum2dlem1  16451  gsum2dlem2  16452  gsum2d  16453  gsum2dOLD  16454  dprdfinv  16499  dprdfinvOLD  16506  dprdf1  16520  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dprd2db  16532  dpjidcl  16547  dpjidclOLD  16554  ablfac1eulem  16563  ablfac1eu  16564  ablfaclem2  16577  gsumdixpOLD  16690  gsumdixp  16691  subrgid  16847  lcomfsupOLD  16964  lcomfsupp  16965  lss1  17000  lbsextlem1  17219  rlmval2  17255  rlmbas  17256  rlmplusg  17257  rlm0  17258  rlmmulr  17260  rlmsca  17261  rlmsca2  17262  rlmvsca  17263  rlmtopn  17264  rlmds  17265  psrass1lem  17427  mplsubglem  17490  mpllsslem  17491  mplsubglemOLD  17492  mpllsslemOLD  17493  mplsubrglem  17497  mplsubrglemOLD  17498  mplcoe1  17524  mplcoe5  17528  mplbas2  17531  mplbas2OLD  17532  evlslem4OLD  17570  evlslem4  17571  psrbagev1  17574  psrbagev1OLD  17575  evlslem2  17577  ply1coeOLD  17727  znf1o  17964  zntoslem  17969  regsumsupp  18032  css0  18094  frlmip  18183  uvcresum  18198  frlmsslsp  18203  frlmsslspOLD  18204  frlmlbs  18205  frlmup1  18206  mamures  18270  mdetrsca2  18391  mdetrlin2  18393  mdetunilem5  18402  mdetunilem9  18406  smadiadetglem1  18457  smadiadetglem2  18458  topopn  18499  fiinbas  18537  topbas  18557  topcld  18619  clstop  18653  ntrtop  18654  opnneissb  18698  opnssneib  18699  opnneiid  18710  neiptopuni  18714  neiptoptop  18715  maxlp  18731  isperf2  18736  restopn2  18761  restperf  18768  idcn  18841  cnconst2  18867  lmres  18884  rncmp  18979  fiuncmp  18987  cmpfi  18991  concn  19010  1stcelcls  19045  llyidm  19072  nllyidm  19073  toplly  19074  kgentopon  19091  kgencn2  19110  ptpjpre1  19124  ptbasfi  19134  ptcld  19166  xkopt  19208  elqtop2  19254  qtopuni  19255  ptcmpfi  19366  fbssfi  19390  opnfbas  19395  filtop  19408  isfil2  19409  isfild  19411  fsubbas  19420  ssfg  19425  filssufilg  19464  ufileu  19472  imaelfm  19504  rnelfm  19506  fmfnfmlem4  19510  neiflim  19527  supnfcls  19573  fclscf  19578  flimfnfcls  19581  tsmsfbas  19678  utopbas  19790  xpsxmet  19935  xpsdsval  19936  xpsmet  19937  tmsxms  20041  tmsms  20042  imasf1oxms  20044  imasf1oms  20045  prdsxms  20085  prdsms  20086  tmsxpsval  20093  retopbas  20319  cnngp  20339  cnperf  20377  retopcon  20386  fsumcn  20426  abscncf  20457  recncf  20458  imcncf  20459  cjcncf  20460  mulc1cncf  20461  cncfcn1  20466  cncfmpt2f  20470  cncfmpt2ss  20471  addccncf  20472  cdivcncf  20473  negcncf  20474  negfcncf  20475  abscncfALT  20476  cnmpt2pc  20480  xrhmeo  20498  oprpiece1res1  20503  oprpiece1res2  20504  cnrehmeo  20505  iscau3  20769  caubl  20798  caublcls  20799  rrxip  20874  rrxcph  20876  rrxmval  20884  rrxdstprj1  20888  evthicc2  20924  ovolre  20988  volsuplem  21016  uniiccdif  21038  uniioovol  21039  uniiccvol  21040  uniioombllem3  21045  uniioombllem4  21046  uniioombllem5  21047  dyadmbllem  21059  volcn  21066  volivth  21067  itgfsum  21284  iblabslem  21285  iblabs  21286  bddmulibl  21296  cnlimc  21343  cnlimci  21344  dvres3  21368  dvres3a  21369  dvidlem  21370  dvcnp2  21374  dvcn  21375  dvnadd  21383  dvnres  21385  cpnord  21389  cpnres  21391  dvaddbr  21392  dvmulbr  21393  dvcmul  21398  dvcmulf  21399  dvcobr  21400  dvcjbr  21403  dvrec  21409  dvmptntr  21425  dvmptfsum  21427  dveflem  21431  dvef  21432  rolle  21442  dvlipcn  21446  c1liplem1  21448  dvgt0lem2  21455  dvivth  21462  lhop1lem  21465  dvfsumabs  21475  ftc1a  21489  ftc1cn  21495  ftc2  21496  deg1mul3le  21568  plyssc  21648  plyeq0  21659  coeeulem  21672  0dgr  21693  coemulc  21702  coe0  21703  coesub  21704  coe1termlem  21705  dgrmulc  21718  dgrsub  21719  dgrcolem1  21720  dgrcolem2  21721  dvnply2  21733  plycpn  21735  plyremlem  21750  fta1lem  21753  vieta1lem2  21757  aalioulem3  21780  dvntaylp  21816  taylthlem1  21818  taylthlem2  21819  ulmcn  21844  psercn  21871  pserdv  21874  abelth  21886  efcn  21888  efcvx  21894  pige3  21959  dvrelog  22062  logcn  22072  dvloglem  22073  dvlog  22076  dvlog2  22078  efopnlem2  22082  logccv  22088  cxpcn  22163  cxpcn2  22164  cxpcn3  22166  resqrcn  22167  sqrcn  22168  loglesqr  22176  atancn  22311  rlimcnp3  22341  jensen  22362  ftalem3  22392  basellem2  22399  dchrfi  22574  dchrisumlema  22717  pntrsumo1  22794  pntrsumbnd  22795  pntlem3  22838  cusgrasizeindslem2  23350  efghgrp  23828  sspid  24091  ssps  24096  helch  24614  hhssnv  24633  hhsssh  24638  shintcl  24701  chintcl  24703  shlesb1i  24757  omlsi  24775  chlejb1i  24847  chm0i  24861  chabs1  24887  chabs2  24888  spanun  24916  cmidi  24981  pjidmcoi  25549  csmdsymi  25706  sumdmdlem2  25791  dmdbr5ati  25794  mdcompli  25801  dmdcompli  25802  disjdifprg  25887  xppreima  25932  xrinfm  26016  clatp0cl  26100  clatp1cl  26101  xrsmulgzz  26107  xrsp0  26110  xrsp1  26111  gsumle  26214  gsummpt2co  26217  gsumvsca1  26219  gsumvsca2  26220  pnfneige0  26350  esumsn  26484  esumcvg  26504  pwsiga  26542  sigagenid  26563  lgamgulmlem2  26985  cvmlift2lem6  27166  relexpdm  27306  relexprn  27307  rtrclreclem.refl  27315  rtrclreclem.subset  27316  prodmolem3  27415  iprod  27420  iprodn0  27422  fprodss  27430  fprodcl  27434  fprod2d  27461  risefaccl  27487  fallfaccl  27488  trpredtr  27663  trpredpo  27668  wzel  27730  frrlem5c  27743  frrlem10  27748  imagesset  27953  ontgval  28247  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  ovoliunnfl  28404  voliunnfl  28406  volsupnfl  28407  mbfposadd  28410  ftc1cnnclem  28436  ftc1cnnc  28437  ftc1anc  28446  ftc2nc  28447  areacirclem2  28456  areacirclem3  28457  areacirclem4  28458  areacirc  28460  ivthALT  28501  fness  28525  ssref  28526  fneref  28527  refref  28528  refssfne  28537  fnemeet1  28558  fnejoin2  28561  filnetlem2  28571  filnetlem4  28573  welb  28601  caures  28627  constcncf  28629  idcncf  28630  sub1cncf  28631  sub2cncf  28632  cnresima  28634  rngoidl  28795  ismrcd1  29005  ismrc  29008  incssnn0  29018  mzpclall  29034  rmydioph  29334  rmxdioph  29336  expdiophlem2  29342  expdioph  29343  aomclem6  29383  kelac1  29387  gicabl  29425  rgspnid  29500  itgpowd  29561  arearect  29562  areaquad  29563  lhe4.4ex1a  29574  dvsconst  29575  dvsid  29576  dvsef  29577  dvconstbi  29579  dvcosre  29759  itgsinexplem1  29765  funresfunco  30002  onfrALTlem3  31181  onfrALTlem3VD  31552  bnj1253  31937  bj-rabtr  32332  bj-rabtrAUTO  32334  atpsubN  33290  pol1N  33447  1psubclN  33481  cdlemefrs32fva  33937  dia2dimlem13  34614  dibord  34697  dochvalr  34895  hdmapevec  35376
  Copyright terms: Public domain W3C validator