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

Theorem ssid 3480
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 23 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3465 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  eqimssi  3515  eqimss2i  3516  nsspssun  3703  inv1  3786  disjpss  3840  difid  3860  pwidg  3989  elssuni  4242  unimax  4248  intmin  4269  rintn0  4387  sseliALT  4549  xpss1  4954  xpss2  4955  residm  5147  resdm  5157  resmpt3  5166  ssrnres  5286  ordunidif  5481  dffn3  5744  fdmrn  5752  fvreseq1  5989  fimacnv  6018  iunpw  6610  onsucuni  6660  tfisi  6690  fparlem3  6900  fparlem4  6901  funsssuppss  6943  suppofss1d  6954  suppofss2d  6955  tfrlem1  7093  tz7.48-2  7158  oaordi  7246  omwordi  7271  omass  7280  nnaordi  7318  nnmwordi  7335  fpmg  7496  ralxpmap  7520  boxcutc  7564  domss2  7728  0fin  7796  en1eqsn  7798  findcard2d  7810  fimax2g  7814  domunfican  7841  pwfi  7866  fissuni  7876  fipreima  7877  fsuppmptif  7910  fsuppco2  7913  fsuppcor  7914  mapfienlem1  7915  mapfienlem2  7916  wofib  8051  wemapso  8057  noinfep  8155  cantnfval2  8164  cantnfp1lem3  8175  cantnflem1  8184  tcidm  8220  tc0  8221  r1rankidb  8265  r1pw  8306  rankr1id  8323  scott0  8347  htalem  8357  xpomen  8436  infpwfien  8482  alephsmo  8522  dfac12lem3  8564  ackbij2lem4  8661  cflem  8665  cflecard  8672  cflim2  8682  cfslb  8685  fin4en1  8728  fin23lem13  8751  fin23lem15  8753  fin23lem36  8767  isf32lem1  8772  fin67  8814  dcomex  8866  zorn2lem4  8918  alephexp2  8995  fpwwe2lem13  9056  canthnumlem  9062  wunex2  9152  wuncidm  9160  eltsk2g  9165  axgroth6  9242  axgroth3  9245  xrsup  12081  expcl  12276  hashcard  12523  hashf1lem2  12603  xptrrel  13012  cotrtrclfv  13044  rtrclreclem1  13089  rtrclreclem2  13090  lo1eq  13599  rlimeq  13600  serclim0  13608  isercolllem2  13696  isercoll  13698  summolem3  13747  isum  13752  fsumser  13763  fsumcl  13766  fsum2d  13799  fsumabs  13828  fsumrlim  13838  fsumo1  13839  fsumiun  13848  flo1  13879  prodmolem3  13954  iprod  13959  iprodn0  13961  fprodss  13969  fprodcl  13973  fprod2d  14002  fprodclf  14013  risefaccl  14035  fallfaccl  14036  eflt  14138  rpnnen2lem3  14236  rpnnen2lem5  14238  rpnnen2lem11  14244  rpnnen2  14245  rexpen  14247  eulerthlem2  14688  ressid  15136  ressinbas  15137  mremre  15454  catsubcat  15688  yon11  16093  yon12  16094  yon2  16095  yonpropd  16097  oppcyon  16098  yonffth  16113  oduclatb  16334  ipopos  16350  fpwipodrs  16354  submid  16542  mulgnncl  16717  mulgnn0cl  16718  mulgcl  16719  subgid  16763  cntrnsg  16939  symggen  17055  sylow3lem5  17211  lsmss1  17244  lsmss2  17246  gsumzres  17471  gsumzcl2  17472  gsumzf1o  17474  gsumadd  17484  gsumzmhm  17498  gsumzoppg  17505  gsum2dlem1  17530  gsum2dlem2  17531  gsum2d  17532  dprdfinv  17580  dprdf1  17594  dmdprdsplitlem  17598  dprd2db  17604  dpjidcl  17619  ablfac1eulem  17633  ablfac1eu  17634  ablfaclem2  17647  gsumdixp  17765  subrgid  17938  lcomfsupp  18056  lss1  18090  lbsextlem1  18309  rlmval2  18345  rlmbas  18346  rlmplusg  18347  rlm0  18348  rlmmulr  18350  rlmsca  18351  rlmsca2  18352  rlmvsca  18353  rlmtopn  18354  rlmds  18355  psrass1lem  18529  mplsubglem  18586  mpllsslem  18587  mplsubrglem  18591  mplcoe1  18617  mplcoe5  18620  mplbas2  18622  evlslem4  18659  psrbagev1  18661  evlslem2  18663  ply1coeOLD  18818  znf1o  19046  zntoslem  19051  regsumsupp  19114  css0  19176  uvcresum  19275  frlmsslsp  19278  frlmlbs  19279  frlmup1  19280  mamures  19339  mdetrsca2  19553  mdetrlin2  19556  mdetunilem5  19565  mdetunilem9  19569  smadiadetglem1  19620  smadiadetglem2  19621  pmatcollpw3  19732  cpmadumatpolylem2  19830  topopn  19860  fiinbas  19891  topbas  19912  topcld  19974  clstop  20009  ntrtop  20010  opnneissb  20054  opnssneib  20055  opnneiid  20066  neiptopuni  20070  neiptoptop  20071  maxlp  20087  isperf2  20092  restopn2  20117  restperf  20124  idcn  20197  cnconst2  20223  lmres  20240  rncmp  20335  fiuncmp  20343  cmpfi  20347  concn  20365  1stcelcls  20400  llyidm  20427  nllyidm  20428  toplly  20429  ssref  20451  refref  20452  kgentopon  20477  kgencn2  20496  ptpjpre1  20510  ptbasfi  20520  ptcld  20552  xkopt  20594  elqtop2  20640  qtopuni  20641  ptcmpfi  20752  fbssfi  20776  opnfbas  20781  filtop  20794  isfil2  20795  isfild  20797  fsubbas  20806  ssfg  20811  filssufilg  20850  ufileu  20858  imaelfm  20890  rnelfm  20892  fmfnfmlem4  20896  neiflim  20913  supnfcls  20959  fclscf  20964  flimfnfcls  20967  tsmsfbas  21066  utopbas  21174  xpsxmet  21319  xpsdsval  21320  xpsmet  21321  tmsxms  21425  tmsms  21426  imasf1oxms  21428  imasf1oms  21429  prdsxms  21469  prdsms  21470  tmsxpsval  21477  retopbas  21685  cnngp  21704  cnperf  21742  retopcon  21751  fsumcn  21791  abscncf  21822  recncf  21823  imcncf  21824  cjcncf  21825  mulc1cncf  21826  cncfcn1  21831  cncfmpt2f  21835  cncfmpt2ss  21836  addccncf  21837  cdivcncf  21838  negcncf  21839  negfcncf  21840  abscncfALT  21841  cnmpt2pc  21845  xrhmeo  21863  oprpiece1res1  21868  oprpiece1res2  21869  cnrehmeo  21870  iscau3  22134  caubl  22163  caublcls  22164  rrxcph  22237  rrxmval  22245  rrxdstprj1  22249  evthicc2  22285  ovolre  22353  volsuplem  22382  uniiccdif  22409  uniioovol  22410  uniiccvol  22411  uniioombllem3  22417  uniioombllem4  22418  uniioombllem5  22419  dyadmbllem  22431  volcn  22438  volivth  22439  itgfsum  22658  iblabslem  22659  iblabs  22660  bddmulibl  22670  cnlimc  22717  cnlimci  22718  dvres3  22742  dvres3a  22743  dvidlem  22744  dvcnp2  22748  dvcn  22749  dvnadd  22757  dvnres  22759  cpnord  22763  cpnres  22765  dvaddbr  22766  dvmulbr  22767  dvcmul  22772  dvcmulf  22773  dvcobr  22774  dvcjbr  22777  dvrec  22783  dvmptntr  22799  dvmptfsum  22801  dveflem  22805  dvef  22806  rolle  22816  dvlipcn  22820  c1liplem1  22822  dvgt0lem2  22829  dvivth  22836  lhop1lem  22839  dvfsumabs  22849  ftc1a  22863  ftc1cn  22869  ftc2  22870  deg1mul3le  22939  plyssc  23019  plyeq0  23030  coeeulem  23043  0dgr  23064  coemulc  23074  coe0  23075  coesub  23076  coe1termlem  23077  dgrmulc  23090  dgrsub  23091  dgrcolem1  23092  dgrcolem2  23093  dvnply2  23105  plycpn  23107  plyremlem  23122  fta1lem  23125  vieta1lem2  23129  aalioulem3  23152  dvntaylp  23188  taylthlem1  23190  taylthlem2  23191  ulmcn  23216  psercn  23243  pserdv  23246  abelth  23258  efcn  23260  efcvx  23266  pige3  23334  dvrelog  23444  logcn  23454  dvloglem  23455  dvlog  23458  dvlog2  23460  efopnlem2  23464  logccv  23470  cxpcn  23547  cxpcn2  23548  cxpcn3  23550  resqrtcn  23551  sqrtcn  23552  loglesqrt  23560  atancn  23724  rlimcnp3  23755  jensen  23776  lgamgulmlem2  23817  ftalem3  23861  basellem2  23868  dchrfi  24043  dchrisumlema  24186  pntrsumo1  24263  pntrsumbnd  24264  pntlem3  24307  cusgrasizeindslem2  25044  efghgrpOLD  25943  sspid  26206  ssps  26211  helch  26728  hhssnv  26747  hhsssh  26752  shintcl  26815  chintcl  26817  shlesb1i  26871  omlsi  26889  chlejb1i  26961  chm0i  26975  chabs1  27001  chabs2  27002  spanun  27030  cmidi  27095  pjidmcoi  27662  csmdsymi  27819  sumdmdlem2  27904  dmdbr5ati  27907  mdcompli  27914  dmdcompli  27915  disjdifprg  28021  fcoinver  28050  xppreima  28085  padct  28147  xrinfm  28172  clatp0cl  28267  clatp1cl  28268  xrsmulgzz  28274  xrsp0  28277  xrsp1  28278  gsumle  28377  gsummpt2co  28378  gsumvsca1  28381  gsumvsca2  28382  mdetpmtr1  28485  reff  28502  locfinreflem  28503  pnfneige0  28593  esumsnf  28721  esumcvg  28743  pwsiga  28788  sigagenid  28809  baselcarsg  28964  bnj1253  29611  cvmlift2lem6  29816  mrsubrn  29936  mrsubff1  29937  mrsub0  29939  mrsubccat  29941  mrsubcn  29942  elmrsubrn  29943  elmsubrn  29951  msubrn  29952  msubff1  29979  mthmpps  30005  trpredtr  30255  trpredpo  30260  wzel  30291  frrlem5c  30304  frrlem10  30309  imagesset  30502  ivthALT  30773  fness  30787  fneref  30788  refssfne  30796  fnemeet1  30804  fnejoin2  30807  filnetlem2  30817  filnetlem4  30819  ontgval  30873  bj-rabtr  31280  bj-rabtrAUTO  31282  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  ovoliunnfl  31686  voliunnfl  31688  volsupnfl  31689  mbfposadd  31692  ftc1cnnclem  31719  ftc1cnnc  31720  ftc1anc  31729  ftc2nc  31730  areacirclem2  31737  areacirclem3  31738  areacirclem4  31739  areacirc  31741  welb  31767  caures  31793  constcncf  31795  idcncf  31796  sub1cncf  31797  sub2cncf  31798  cnresima  31800  rngoidl  31961  atpsubN  33027  pol1N  33184  1psubclN  33218  cdlemefrs32fva  33676  dia2dimlem13  34353  dibord  34436  dochvalr  34634  hdmapevec  35115  ismrcd1  35249  ismrc  35252  incssnn0  35262  mzpclall  35278  rmydioph  35579  rmxdioph  35581  expdiophlem2  35587  expdioph  35588  aomclem6  35627  kelac1  35631  gicabl  35667  rgspnid  35741  itgpowd  35802  arearect  35803  areaquad  35804  fvilbd  35924  relexp0a  35951  brfvrtrcld  35969  corcltrcl  35974  wnefimgd  36241  wfximgfd  36246  extoimad  36248  funfvima2d  36253  nzss  36307  lhe4.4ex1a  36319  dvsconst  36320  dvsid  36321  dvsef  36322  dvconstbi  36324  binomcxplemnn0  36339  onfrALTlem3  36551  onfrALTlem3VD  36928  cnopn  37019  unisn0  37039  founiiun  37073  founiiun0  37092  evthiccabs  37182  islptre  37275  cncfshift  37327  addccncf2  37329  fsumcncf  37331  cncfperiod  37332  negcncfg  37334  cncfcompt  37336  ioccncflimc  37339  cncfuni  37340  icccncfext  37341  cncficcgt0  37342  icocncflimc  37343  cncfiooicclem1  37347  cncfiooicc  37348  cncfiooiccre  37349  cxpcncf2  37354  fprodcncf  37355  dvcosre  37357  dvcnre  37362  fperdvper  37366  dvmptresicc  37367  dvmptfprod  37393  itgsinexplem1  37403  itgcoscmulx  37419  ibliooicc  37421  itgsincmulx  37424  itgsubsticclem  37425  itgiccshift  37430  itgperiod  37431  itgsbtaddcnst  37432  dirkeritg  37537  dirkercncflem2  37539  dirkercncflem4  37541  fourierdlem16  37558  fourierdlem18  37560  fourierdlem21  37563  fourierdlem22  37564  fourierdlem23  37565  fourierdlem32  37574  fourierdlem33  37575  fourierdlem39  37581  fourierdlem40  37582  fourierdlem57  37599  fourierdlem58  37600  fourierdlem59  37601  fourierdlem62  37604  fourierdlem68  37610  fourierdlem72  37614  fourierdlem73  37615  fourierdlem74  37616  fourierdlem75  37617  fourierdlem76  37618  fourierdlem78  37620  fourierdlem83  37625  fourierdlem84  37626  fourierdlem85  37627  fourierdlem88  37630  fourierdlem93  37635  fourierdlem94  37636  fourierdlem95  37637  fourierdlem97  37639  fourierdlem101  37643  fourierdlem103  37645  fourierdlem104  37646  fourierdlem111  37653  fourierdlem112  37654  fourierdlem113  37655  sqwvfoura  37664  sqwvfourb  37665  fouriersw  37667  fouriercn  37668  etransclem18  37688  etransclem22  37692  etransclem34  37704  etransclem46  37716  etransclem47  37717  sge0fsum  37767  funresfunco  38030  submgmid  38564  rnghmsscmap2  38746  rhmsscmap2  38792  srhmsubc  38849  fldhmsubc  38857  srhmsubcALTV  38868  fldhmsubcALTV  38876  elbigolo1  39142
  Copyright terms: Public domain W3C validator