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

Theorem ssid 3473
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 3458 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  eqimssi  3508  eqimss2i  3509  nsspssun  3681  inv1  3762  disjpss  3827  difid  3845  pwidg  3971  elssuni  4219  unimax  4225  intmin  4246  rintn0  4359  sseliALT  4521  ordunidif  4865  xpss1  5046  xpss2  5047  residm  5239  resdm  5246  resmpt3  5255  ssrnres  5374  dffn3  5664  fdmrn  5671  fvreseq1  5903  fimacnv  5934  iunpw  6490  onsucuni  6539  tfisi  6569  fparlem3  6774  fparlem4  6775  funsssuppss  6815  suppofss1d  6826  suppofss2d  6827  tfrlem1  6935  tz7.48-2  6997  oaordi  7085  omwordi  7110  omass  7119  nnaordi  7157  nnmwordi  7174  fpmg  7338  ralxpmap  7362  boxcutc  7406  domss2  7570  0fin  7641  en1eqsn  7643  findcard2d  7655  fimax2g  7659  domunfican  7685  pwfi  7707  fissuni  7717  fipreima  7718  fsuppmptif  7750  fsuppco2  7753  fsuppcor  7754  mapfienlem1  7755  mapfienlem2  7756  wofib  7860  wemapso  7866  sucprcregOLD  7916  noinfep  7966  noinfepOLD  7967  cantnfval2  7978  cantnfp1lem3  7989  cantnflem1d  7997  cantnflem1  7998  cantnfval2OLD  8008  cantnfp1lem3OLD  8015  tcidm  8067  tc0  8068  r1rankidb  8112  r1pw  8153  rankr1id  8170  scott0  8194  htalem  8204  xpomen  8283  infpwfien  8333  alephsmo  8373  dfac12lem3  8415  ackbij2lem4  8512  cflem  8516  cflecard  8523  cflim2  8533  cfslb  8536  fin4en1  8579  fin23lem13  8602  fin23lem15  8604  fin23lem36  8618  isf32lem1  8623  fin67  8665  dcomex  8717  zorn2lem4  8769  alephexp2  8846  fpwwe2lem13  8910  canthnumlem  8916  wunex2  9006  wuncidm  9014  eltsk2g  9019  axgroth6  9096  axgroth3  9099  xrsup  11808  expcl  11984  hashcard  12226  hashf1lem2  12311  lo1eq  13148  rlimeq  13149  serclim0  13157  isercolllem2  13245  isercoll  13247  summolem3  13293  isum  13298  fsumser  13309  fsumcl  13312  fsum2d  13340  fsumabs  13366  fsumrlim  13376  fsumo1  13377  fsumiun  13386  flo1  13419  eflt  13503  xpnnenOLD  13594  rpnnen2lem3  13601  rpnnen2lem5  13603  rpnnen2lem11  13609  rpnnen2  13610  rexpen  13612  eulerthlem2  13959  ressid  14335  ressinbas  14336  mremre  14644  yon11  15176  yon12  15177  yon2  15178  yonpropd  15180  oppcyon  15181  yonffth  15196  oduclatb  15416  ipopos  15432  fpwipodrs  15436  submid  15581  mulgnncl  15744  mulgnn0cl  15745  mulgcl  15746  subgid  15785  cntrnsg  15961  symggen  16078  sylow3lem5  16234  lsmss1  16267  lsmss2  16269  gsumzres  16492  gsumzcl2  16493  gsumzf1o  16495  gsumzresOLD  16496  gsumzclOLD  16497  gsumzf1oOLD  16498  gsumadd  16516  gsumaddOLD  16517  gsumzsplitOLD  16523  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzoppg  16545  gsumzoppgOLD  16546  gsumzinvOLD  16548  gsumsubOLD  16553  gsum2dlem1  16566  gsum2dlem2  16567  gsum2d  16568  gsum2dOLD  16569  dprdfinv  16614  dprdfinvOLD  16621  dprdf1  16635  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprd2db  16647  dpjidcl  16662  dpjidclOLD  16669  ablfac1eulem  16678  ablfac1eu  16679  ablfaclem2  16692  gsumdixpOLD  16806  gsumdixp  16807  subrgid  16973  lcomfsupOLD  17090  lcomfsupp  17091  lss1  17126  lbsextlem1  17345  rlmval2  17381  rlmbas  17382  rlmplusg  17383  rlm0  17384  rlmmulr  17386  rlmsca  17387  rlmsca2  17388  rlmvsca  17389  rlmtopn  17390  rlmds  17391  psrass1lem  17553  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  mplsubrglem  17624  mplsubrglemOLD  17625  mplcoe1  17651  mplcoe5  17655  mplbas2  17658  mplbas2OLD  17659  evlslem4OLD  17697  evlslem4  17698  psrbagev1  17701  psrbagev1OLD  17702  evlslem2  17704  ply1coeOLD  17856  znf1o  18093  zntoslem  18098  regsumsupp  18161  css0  18223  frlmip  18312  uvcresum  18327  frlmsslsp  18332  frlmsslspOLD  18333  frlmlbs  18334  frlmup1  18335  mamures  18399  mdetrsca2  18526  mdetrlin2  18529  mdetunilem5  18538  mdetunilem9  18542  smadiadetglem1  18593  smadiadetglem2  18594  topopn  18635  fiinbas  18673  topbas  18693  topcld  18755  clstop  18789  ntrtop  18790  opnneissb  18834  opnssneib  18835  opnneiid  18846  neiptopuni  18850  neiptoptop  18851  maxlp  18867  isperf2  18872  restopn2  18897  restperf  18904  idcn  18977  cnconst2  19003  lmres  19020  rncmp  19115  fiuncmp  19123  cmpfi  19127  concn  19146  1stcelcls  19181  llyidm  19208  nllyidm  19209  toplly  19210  kgentopon  19227  kgencn2  19246  ptpjpre1  19260  ptbasfi  19270  ptcld  19302  xkopt  19344  elqtop2  19390  qtopuni  19391  ptcmpfi  19502  fbssfi  19526  opnfbas  19531  filtop  19544  isfil2  19545  isfild  19547  fsubbas  19556  ssfg  19561  filssufilg  19600  ufileu  19608  imaelfm  19640  rnelfm  19642  fmfnfmlem4  19646  neiflim  19663  supnfcls  19709  fclscf  19714  flimfnfcls  19717  tsmsfbas  19814  utopbas  19926  xpsxmet  20071  xpsdsval  20072  xpsmet  20073  tmsxms  20177  tmsms  20178  imasf1oxms  20180  imasf1oms  20181  prdsxms  20221  prdsms  20222  tmsxpsval  20229  retopbas  20455  cnngp  20475  cnperf  20513  retopcon  20522  fsumcn  20562  abscncf  20593  recncf  20594  imcncf  20595  cjcncf  20596  mulc1cncf  20597  cncfcn1  20602  cncfmpt2f  20606  cncfmpt2ss  20607  addccncf  20608  cdivcncf  20609  negcncf  20610  negfcncf  20611  abscncfALT  20612  cnmpt2pc  20616  xrhmeo  20634  oprpiece1res1  20639  oprpiece1res2  20640  cnrehmeo  20641  iscau3  20905  caubl  20934  caublcls  20935  rrxip  21010  rrxcph  21012  rrxmval  21020  rrxdstprj1  21024  evthicc2  21060  ovolre  21124  volsuplem  21152  uniiccdif  21174  uniioovol  21175  uniiccvol  21176  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  dyadmbllem  21195  volcn  21202  volivth  21203  itgfsum  21420  iblabslem  21421  iblabs  21422  bddmulibl  21432  cnlimc  21479  cnlimci  21480  dvres3  21504  dvres3a  21505  dvidlem  21506  dvcnp2  21510  dvcn  21511  dvnadd  21519  dvnres  21521  cpnord  21525  cpnres  21527  dvaddbr  21528  dvmulbr  21529  dvcmul  21534  dvcmulf  21535  dvcobr  21536  dvcjbr  21539  dvrec  21545  dvmptntr  21561  dvmptfsum  21563  dveflem  21567  dvef  21568  rolle  21578  dvlipcn  21582  c1liplem1  21584  dvgt0lem2  21591  dvivth  21598  lhop1lem  21601  dvfsumabs  21611  ftc1a  21625  ftc1cn  21631  ftc2  21632  deg1mul3le  21704  plyssc  21784  plyeq0  21795  coeeulem  21808  0dgr  21829  coemulc  21838  coe0  21839  coesub  21840  coe1termlem  21841  dgrmulc  21854  dgrsub  21855  dgrcolem1  21856  dgrcolem2  21857  dvnply2  21869  plycpn  21871  plyremlem  21886  fta1lem  21889  vieta1lem2  21893  aalioulem3  21916  dvntaylp  21952  taylthlem1  21954  taylthlem2  21955  ulmcn  21980  psercn  22007  pserdv  22010  abelth  22022  efcn  22024  efcvx  22030  pige3  22095  dvrelog  22198  logcn  22208  dvloglem  22209  dvlog  22212  dvlog2  22214  efopnlem2  22218  logccv  22224  cxpcn  22299  cxpcn2  22300  cxpcn3  22302  resqrcn  22303  sqrcn  22304  loglesqr  22312  atancn  22447  rlimcnp3  22477  jensen  22498  ftalem3  22528  basellem2  22535  dchrfi  22710  dchrisumlema  22853  pntrsumo1  22930  pntrsumbnd  22931  pntlem3  22974  cusgrasizeindslem2  23517  efghgrp  23995  sspid  24258  ssps  24263  helch  24781  hhssnv  24800  hhsssh  24805  shintcl  24868  chintcl  24870  shlesb1i  24924  omlsi  24942  chlejb1i  25014  chm0i  25028  chabs1  25054  chabs2  25055  spanun  25083  cmidi  25148  pjidmcoi  25716  csmdsymi  25873  sumdmdlem2  25958  dmdbr5ati  25961  mdcompli  25968  dmdcompli  25969  disjdifprg  26053  xppreima  26098  xrinfm  26182  clatp0cl  26266  clatp1cl  26267  xrsmulgzz  26273  xrsp0  26276  xrsp1  26277  gsumle  26380  gsummpt2co  26383  gsumvsca1  26385  gsumvsca2  26386  pnfneige0  26515  esumsn  26649  esumcvg  26669  pwsiga  26707  sigagenid  26728  lgamgulmlem2  27150  cvmlift2lem6  27331  relexpdm  27471  relexprn  27472  rtrclreclem.refl  27480  rtrclreclem.subset  27481  prodmolem3  27580  iprod  27585  iprodn0  27587  fprodss  27595  fprodcl  27599  fprod2d  27626  risefaccl  27652  fallfaccl  27653  trpredtr  27828  trpredpo  27833  wzel  27895  frrlem5c  27908  frrlem10  27913  imagesset  28118  ontgval  28411  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  mbfposadd  28577  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anc  28613  ftc2nc  28614  areacirclem2  28623  areacirclem3  28624  areacirclem4  28625  areacirc  28627  ivthALT  28668  fness  28692  ssref  28693  fneref  28694  refref  28695  refssfne  28704  fnemeet1  28725  fnejoin2  28728  filnetlem2  28738  filnetlem4  28740  welb  28768  caures  28794  constcncf  28796  idcncf  28797  sub1cncf  28798  sub2cncf  28799  cnresima  28801  rngoidl  28962  ismrcd1  29172  ismrc  29175  incssnn0  29185  mzpclall  29201  rmydioph  29501  rmxdioph  29503  expdiophlem2  29509  expdioph  29510  aomclem6  29550  kelac1  29554  gicabl  29592  rgspnid  29667  itgpowd  29728  arearect  29729  areaquad  29730  lhe4.4ex1a  29741  dvsconst  29742  dvsid  29743  dvsef  29744  dvconstbi  29746  dvcosre  29926  itgsinexplem1  29932  funresfunco  30169  pmatcollpw4fi  31241  onfrALTlem3  31552  onfrALTlem3VD  31923  bnj1253  32308  bj-rabtr  32732  bj-rabtrAUTO  32734  atpsubN  33703  pol1N  33860  1psubclN  33894  cdlemefrs32fva  34350  dia2dimlem13  35027  dibord  35110  dochvalr  35308  hdmapevec  35789
  Copyright terms: Public domain W3C validator