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

Theorem ssid 3463
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 3448 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  eqimssi  3498  eqimss2i  3499  nsspssun  3688  inv1  3773  disjpss  3827  difid  3847  pwidg  3976  elssuni  4241  unimax  4247  intmin  4268  rintn0  4388  sseliALT  4552  xpss1  4965  xpss2  4966  residm  5158  resdm  5168  resmpt3  5177  ssrnres  5297  ordunidif  5494  dffn3  5763  fdmrn  5771  fvreseq1  6011  fimacnv  6040  iunpw  6637  onsucuni  6687  tfisi  6717  fparlem3  6930  fparlem4  6931  funsssuppss  6973  suppofss1d  6984  suppofss2d  6985  tfrlem1  7125  tz7.48-2  7190  oaordi  7278  omwordi  7303  omass  7312  nnaordi  7350  nnmwordi  7367  fpmg  7528  ralxpmap  7552  boxcutc  7596  domss2  7762  0fin  7830  en1eqsn  7832  findcard2d  7844  fimax2g  7848  domunfican  7875  pwfi  7900  fissuni  7910  fipreima  7911  fsuppmptif  7944  fsuppco2  7947  fsuppcor  7948  mapfienlem1  7949  mapfienlem2  7950  fimin2g  8044  wofib  8091  wemapso  8097  noinfep  8196  cantnfval2  8205  cantnfp1lem3  8216  cantnflem1  8225  tcidm  8261  tc0  8262  r1rankidb  8306  r1pw  8347  rankr1id  8364  scott0  8388  htalem  8398  xpomen  8477  infpwfien  8524  alephsmo  8564  dfac12lem3  8606  ackbij2lem4  8703  cflem  8707  cflecard  8714  cflim2  8724  cfslb  8727  fin4en1  8770  fin23lem13  8793  fin23lem15  8795  fin23lem36  8809  isf32lem1  8814  fin67  8856  dcomex  8908  zorn2lem4  8960  alephexp2  9037  fpwwe2lem13  9098  canthnumlem  9104  wunex2  9194  wuncidm  9202  eltsk2g  9207  axgroth6  9284  axgroth3  9287  xrsup  12133  expcl  12328  hashcard  12575  hashf1lem2  12658  xptrrel  13099  cotrtrclfv  13131  rtrclreclem1  13176  rtrclreclem2  13177  lo1eq  13687  rlimeq  13688  serclim0  13696  isercolllem2  13784  isercoll  13786  summolem3  13835  isum  13840  fsumser  13851  fsumcl  13854  fsum2d  13887  fsumabs  13916  fsumrlim  13926  fsumo1  13927  fsumiun  13936  flo1  13967  prodmolem3  14042  iprod  14047  iprodn0  14049  fprodss  14057  fprodcl  14061  fprod2d  14090  fprodclf  14101  risefaccl  14123  fallfaccl  14124  eflt  14226  rpnnen2lem3  14324  rpnnen2lem5  14326  rpnnen2lem11  14332  rpnnen2  14333  rexpen  14335  eulerthlem2  14785  ressid  15239  ressinbas  15240  mremre  15565  catsubcat  15799  yon11  16204  yon12  16205  yon2  16206  yonpropd  16208  oppcyon  16209  yonffth  16224  oduclatb  16445  ipopos  16461  fpwipodrs  16465  submid  16653  mulgnncl  16828  mulgnn0cl  16829  mulgcl  16830  subgid  16874  cntrnsg  17050  symggen  17166  sylow3lem5  17338  lsmss1  17371  lsmss2  17373  gsumzres  17598  gsumzcl2  17599  gsumzf1o  17601  gsumadd  17611  gsumzmhm  17625  gsumzoppg  17632  gsum2dlem1  17657  gsum2dlem2  17658  gsum2d  17659  dprdfinv  17707  dprdf1  17721  dmdprdsplitlem  17725  dprd2db  17731  dpjidcl  17746  ablfac1eulem  17760  ablfac1eu  17761  ablfaclem2  17774  gsumdixp  17892  subrgid  18065  lcomfsupp  18183  lss1  18217  lbsextlem1  18436  rlmval2  18472  rlmbas  18473  rlmplusg  18474  rlm0  18475  rlmmulr  18477  rlmsca  18478  rlmsca2  18479  rlmvsca  18480  rlmtopn  18481  rlmds  18482  psrass1lem  18656  mplsubglem  18713  mpllsslem  18714  mplsubrglem  18718  mplcoe1  18744  mplcoe5  18747  mplbas2  18749  evlslem4  18786  psrbagev1  18788  evlslem2  18790  ply1coeOLD  18945  znf1o  19177  zntoslem  19182  regsumsupp  19245  css0  19307  uvcresum  19406  frlmsslsp  19409  frlmlbs  19410  frlmup1  19411  mamures  19470  mdetrsca2  19684  mdetrlin2  19687  mdetunilem5  19696  mdetunilem9  19700  smadiadetglem1  19751  smadiadetglem2  19752  pmatcollpw3  19863  cpmadumatpolylem2  19961  topopn  19991  fiinbas  20022  topbas  20043  topcld  20105  clstop  20140  ntrtop  20141  opnneissb  20185  opnssneib  20186  opnneiid  20197  neiptopuni  20201  neiptoptop  20202  maxlp  20218  isperf2  20223  restopn2  20248  restperf  20255  idcn  20328  cnconst2  20354  lmres  20371  rncmp  20466  fiuncmp  20474  cmpfi  20478  concn  20496  1stcelcls  20531  llyidm  20558  nllyidm  20559  toplly  20560  ssref  20582  refref  20583  kgentopon  20608  kgencn2  20627  ptpjpre1  20641  ptbasfi  20651  ptcld  20683  xkopt  20725  elqtop2  20771  qtopuni  20772  ptcmpfi  20883  fbssfi  20907  opnfbas  20912  filtop  20925  isfil2  20926  isfild  20928  fsubbas  20937  ssfg  20942  filssufilg  20981  ufileu  20989  imaelfm  21021  rnelfm  21023  fmfnfmlem4  21027  neiflim  21044  supnfcls  21090  fclscf  21095  flimfnfcls  21098  tsmsfbas  21197  utopbas  21305  xpsxmet  21450  xpsdsval  21451  xpsmet  21452  tmsxms  21556  tmsms  21557  imasf1oxms  21559  imasf1oms  21560  prdsxms  21600  prdsms  21601  tmsxpsval  21608  retopbas  21836  cnngp  21855  cnperf  21893  retopcon  21902  fsumcn  21957  abscncf  21988  recncf  21989  imcncf  21990  cjcncf  21991  mulc1cncf  21992  cncfcn1  21997  cncfmpt2f  22001  cncfmpt2ss  22002  addccncf  22003  cdivcncf  22004  negcncf  22005  negfcncf  22006  abscncfALT  22007  cnmpt2pc  22011  xrhmeo  22029  oprpiece1res1  22034  oprpiece1res2  22035  cnrehmeo  22036  iscau3  22303  caubl  22332  caublcls  22333  rrxcph  22406  rrxmval  22414  rrxdstprj1  22418  evthicc2  22466  ovolre  22534  volsuplem  22564  uniiccdif  22591  uniioovol  22592  uniiccvol  22593  uniioombllem3  22599  uniioombllem4  22600  uniioombllem5  22601  dyadmbllem  22613  volcn  22620  volivth  22621  itgfsum  22840  iblabslem  22841  iblabs  22842  bddmulibl  22852  cnlimc  22899  cnlimci  22900  dvres3  22924  dvres3a  22925  dvidlem  22926  dvcnp2  22930  dvcn  22931  dvnadd  22939  dvnres  22941  cpnord  22945  cpnres  22947  dvaddbr  22948  dvmulbr  22949  dvcmul  22954  dvcmulf  22955  dvcobr  22956  dvcjbr  22959  dvrec  22965  dvmptntr  22981  dvmptfsum  22983  dveflem  22987  dvef  22988  rolle  22998  dvlipcn  23002  c1liplem1  23004  dvgt0lem2  23011  dvivth  23018  lhop1lem  23021  dvfsumabs  23031  ftc1a  23045  ftc1cn  23051  ftc2  23052  deg1mul3le  23121  plyssc  23210  plyeq0  23221  coeeulem  23234  0dgr  23255  coemulc  23265  coe0  23266  coesub  23267  coe1termlem  23268  dgrmulc  23281  dgrsub  23282  dgrcolem1  23283  dgrcolem2  23284  dvnply2  23296  plycpn  23298  plyremlem  23313  fta1lem  23316  vieta1lem2  23320  aalioulem3  23346  dvntaylp  23382  taylthlem1  23384  taylthlem2  23385  ulmcn  23410  psercn  23437  pserdv  23440  abelth  23452  efcn  23454  efcvx  23460  pige3  23528  dvrelog  23638  logcn  23648  dvloglem  23649  dvlog  23652  dvlog2  23654  efopnlem2  23658  logccv  23664  cxpcn  23741  cxpcn2  23742  cxpcn3  23744  resqrtcn  23745  sqrtcn  23746  loglesqrt  23754  atancn  23918  rlimcnp3  23949  jensen  23970  lgamgulmlem2  24011  ftalem3  24055  basellem2  24064  dchrfi  24239  dchrisumlema  24382  pntrsumo1  24459  pntrsumbnd  24460  pntlem3  24503  cusgrasizeindslem2  25258  efghgrpOLD  26157  sspid  26420  ssps  26425  helch  26952  hhssnv  26971  hhsssh  26976  shintcl  27039  chintcl  27041  shlesb1i  27095  omlsi  27113  chlejb1i  27185  chm0i  27199  chabs1  27225  chabs2  27226  spanun  27254  cmidi  27319  pjidmcoi  27886  csmdsymi  28043  sumdmdlem2  28128  dmdbr5ati  28131  mdcompli  28138  dmdcompli  28139  disjdifprg  28239  fcoinver  28267  xppreima  28301  padct  28359  xrinfm  28385  xrinfmOLD  28386  clatp0cl  28485  clatp1cl  28486  xrsmulgzz  28492  xrsp0  28495  xrsp1  28496  gsumle  28593  gsummpt2co  28594  gsumvsca1  28596  gsumvsca2  28597  mdetpmtr1  28700  reff  28717  locfinreflem  28718  pnfneige0  28808  esumsnf  28936  esumcvg  28958  pwsiga  29003  sigagenid  29024  baselcarsg  29188  bnj1253  29876  cvmlift2lem6  30081  mrsubrn  30201  mrsubff1  30202  mrsub0  30204  mrsubccat  30206  mrsubcn  30207  elmrsubrn  30208  elmsubrn  30216  msubrn  30217  msubff1  30244  mthmpps  30270  trpredtr  30521  trpredpo  30526  wzel  30557  frrlem5c  30570  frrlem10  30575  imagesset  30770  ivthALT  31041  fness  31055  fneref  31056  refssfne  31064  fnemeet1  31072  fnejoin2  31075  filnetlem2  31085  filnetlem4  31087  ontgval  31141  bj-rabtr  31579  bj-rabtrALTALT  31581  bj-rabtrAUTO  31582  elxp8  31820  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  mbfposadd  32034  ftc1cnnclem  32061  ftc1cnnc  32062  ftc1anc  32071  ftc2nc  32072  areacirclem2  32079  areacirclem3  32080  areacirclem4  32081  areacirc  32083  welb  32109  caures  32135  constcncf  32137  idcncf  32138  sub1cncf  32139  sub2cncf  32140  cnresima  32142  rngoidl  32303  atpsubN  33364  pol1N  33521  1psubclN  33555  cdlemefrs32fva  34013  dia2dimlem13  34690  dibord  34773  dochvalr  34971  hdmapevec  35452  ismrcd1  35586  ismrc  35589  incssnn0  35599  mzpclall  35615  rmydioph  35915  rmxdioph  35917  expdiophlem2  35923  expdioph  35924  aomclem6  35963  kelac1  35967  gicabl  36003  rgspnid  36084  itgpowd  36145  arearect  36146  areaquad  36147  clcnvlem  36276  cnvtrucl0  36277  cnvtrcl0  36279  fvilbd  36327  relexp0a  36354  brfvrtrcld  36372  corcltrcl  36377  wnefimgd  36646  wfximgfd  36651  extoimad  36653  funfvima2d  36658  nzss  36711  lhe4.4ex1a  36723  dvsconst  36724  dvsid  36725  dvsef  36726  dvconstbi  36728  binomcxplemnn0  36743  onfrALTlem3  36955  onfrALTlem3VD  37325  cnopn  37414  unisn0  37433  founiiun  37500  founiiun0  37519  choicefi  37535  evthiccabs  37678  islptre  37785  cncfshift  37837  addccncf2  37839  fsumcncf  37841  cncfperiod  37842  negcncfg  37844  cncfcompt  37846  ioccncflimc  37849  cncfuni  37850  icccncfext  37851  cncficcgt0  37852  icocncflimc  37853  cncfiooicclem1  37857  cncfiooicc  37858  cncfiooiccre  37859  cxpcncf2  37864  fprodcncf  37865  dvcosre  37867  dvcnre  37872  fperdvper  37876  dvmptresicc  37877  dvmptfprod  37906  itgsinexplem1  37916  itgcoscmulx  37932  ibliooicc  37934  itgsincmulx  37937  itgsubsticclem  37938  itgiccshift  37943  itgperiod  37944  itgsbtaddcnst  37945  dirkeritg  38065  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem16  38086  fourierdlem18  38088  fourierdlem21  38091  fourierdlem22  38092  fourierdlem23  38093  fourierdlem32  38103  fourierdlem33  38104  fourierdlem39  38110  fourierdlem40  38111  fourierdlem57  38128  fourierdlem58  38129  fourierdlem59  38130  fourierdlem62  38133  fourierdlem68  38139  fourierdlem72  38143  fourierdlem73  38144  fourierdlem74  38145  fourierdlem75  38146  fourierdlem76  38147  fourierdlem78  38149  fourierdlem83  38154  fourierdlem84  38155  fourierdlem85  38156  fourierdlem88  38159  fourierdlem93  38164  fourierdlem94  38165  fourierdlem95  38166  fourierdlem97  38168  fourierdlem101  38172  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  fourierdlem112  38183  fourierdlem113  38184  sqwvfoura  38193  sqwvfourb  38194  fouriersw  38196  fouriercn  38197  etransclem18  38218  etransclem22  38222  etransclem34  38234  etransclem46  38246  etransclem47  38247  sge0fsum  38332  hoidmvlelem2  38525  hspdifhsp  38545  hspmbllem2  38556  hspmbl  38558  funresfunco  38761  uhgrsubgrself  39498  uhgrspansubgr  39509  nbupgr  39558  nbumgrvtx  39560  nbgr2vtx1edg  39564  cusgrexi  39653  1wlkvtxeledg  39817  upgr11wlkdlem2  39957  1pthon2ve  39965  umgr2adedgwlk  39990  umgr2adedgwlkon  39991  umgr2adedgspth  39993  submgmid  40162  rnghmsscmap2  40344  rhmsscmap2  40390  srhmsubc  40447  fldhmsubc  40455  srhmsubcALTV  40466  fldhmsubcALTV  40474  elbigolo1  40737
  Copyright terms: Public domain W3C validator