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

Theorem ssid 3419
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 3404 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  eqimssi  3454  eqimss2i  3455  nsspssun  3642  inv1  3727  disjpss  3781  difid  3801  pwidg  3930  elssuni  4184  unimax  4190  intmin  4211  rintn0  4329  sseliALT  4493  xpss1  4898  xpss2  4899  residm  5091  resdm  5101  resmpt3  5110  ssrnres  5230  ordunidif  5426  dffn3  5689  fdmrn  5697  fvreseq1  5935  fimacnv  5964  iunpw  6556  onsucuni  6606  tfisi  6636  fparlem3  6846  fparlem4  6847  funsssuppss  6889  suppofss1d  6900  suppofss2d  6901  tfrlem1  7042  tz7.48-2  7107  oaordi  7195  omwordi  7220  omass  7229  nnaordi  7267  nnmwordi  7284  fpmg  7445  ralxpmap  7469  boxcutc  7513  domss2  7677  0fin  7745  en1eqsn  7747  findcard2d  7759  fimax2g  7763  domunfican  7790  pwfi  7815  fissuni  7825  fipreima  7826  fsuppmptif  7859  fsuppco2  7862  fsuppcor  7863  mapfienlem1  7864  mapfienlem2  7865  fimin2g  7959  wofib  8006  wemapso  8012  noinfep  8110  cantnfval2  8119  cantnfp1lem3  8130  cantnflem1  8139  tcidm  8175  tc0  8176  r1rankidb  8220  r1pw  8261  rankr1id  8278  scott0  8302  htalem  8312  xpomen  8391  infpwfien  8437  alephsmo  8477  dfac12lem3  8519  ackbij2lem4  8616  cflem  8620  cflecard  8627  cflim2  8637  cfslb  8640  fin4en1  8683  fin23lem13  8706  fin23lem15  8708  fin23lem36  8722  isf32lem1  8727  fin67  8769  dcomex  8821  zorn2lem4  8873  alephexp2  8950  fpwwe2lem13  9011  canthnumlem  9017  wunex2  9107  wuncidm  9115  eltsk2g  9120  axgroth6  9197  axgroth3  9200  xrsup  12038  expcl  12233  hashcard  12480  hashf1lem2  12560  xptrrel  12981  cotrtrclfv  13013  rtrclreclem1  13058  rtrclreclem2  13059  lo1eq  13568  rlimeq  13569  serclim0  13577  isercolllem2  13665  isercoll  13667  summolem3  13716  isum  13721  fsumser  13732  fsumcl  13735  fsum2d  13768  fsumabs  13797  fsumrlim  13807  fsumo1  13808  fsumiun  13817  flo1  13848  prodmolem3  13923  iprod  13928  iprodn0  13930  fprodss  13938  fprodcl  13942  fprod2d  13971  fprodclf  13982  risefaccl  14004  fallfaccl  14005  eflt  14107  rpnnen2lem3  14205  rpnnen2lem5  14207  rpnnen2lem11  14213  rpnnen2  14214  rexpen  14216  eulerthlem2  14666  ressid  15120  ressinbas  15121  mremre  15446  catsubcat  15680  yon11  16085  yon12  16086  yon2  16087  yonpropd  16089  oppcyon  16090  yonffth  16105  oduclatb  16326  ipopos  16342  fpwipodrs  16346  submid  16534  mulgnncl  16709  mulgnn0cl  16710  mulgcl  16711  subgid  16755  cntrnsg  16931  symggen  17047  sylow3lem5  17219  lsmss1  17252  lsmss2  17254  gsumzres  17479  gsumzcl2  17480  gsumzf1o  17482  gsumadd  17492  gsumzmhm  17506  gsumzoppg  17513  gsum2dlem1  17538  gsum2dlem2  17539  gsum2d  17540  dprdfinv  17588  dprdf1  17602  dmdprdsplitlem  17606  dprd2db  17612  dpjidcl  17627  ablfac1eulem  17641  ablfac1eu  17642  ablfaclem2  17655  gsumdixp  17773  subrgid  17946  lcomfsupp  18064  lss1  18098  lbsextlem1  18317  rlmval2  18353  rlmbas  18354  rlmplusg  18355  rlm0  18356  rlmmulr  18358  rlmsca  18359  rlmsca2  18360  rlmvsca  18361  rlmtopn  18362  rlmds  18363  psrass1lem  18537  mplsubglem  18594  mpllsslem  18595  mplsubrglem  18599  mplcoe1  18625  mplcoe5  18628  mplbas2  18630  evlslem4  18667  psrbagev1  18669  evlslem2  18671  ply1coeOLD  18826  znf1o  19057  zntoslem  19062  regsumsupp  19125  css0  19187  uvcresum  19286  frlmsslsp  19289  frlmlbs  19290  frlmup1  19291  mamures  19350  mdetrsca2  19564  mdetrlin2  19567  mdetunilem5  19576  mdetunilem9  19580  smadiadetglem1  19631  smadiadetglem2  19632  pmatcollpw3  19743  cpmadumatpolylem2  19841  topopn  19871  fiinbas  19902  topbas  19923  topcld  19985  clstop  20020  ntrtop  20021  opnneissb  20065  opnssneib  20066  opnneiid  20077  neiptopuni  20081  neiptoptop  20082  maxlp  20098  isperf2  20103  restopn2  20128  restperf  20135  idcn  20208  cnconst2  20234  lmres  20251  rncmp  20346  fiuncmp  20354  cmpfi  20358  concn  20376  1stcelcls  20411  llyidm  20438  nllyidm  20439  toplly  20440  ssref  20462  refref  20463  kgentopon  20488  kgencn2  20507  ptpjpre1  20521  ptbasfi  20531  ptcld  20563  xkopt  20605  elqtop2  20651  qtopuni  20652  ptcmpfi  20763  fbssfi  20787  opnfbas  20792  filtop  20805  isfil2  20806  isfild  20808  fsubbas  20817  ssfg  20822  filssufilg  20861  ufileu  20869  imaelfm  20901  rnelfm  20903  fmfnfmlem4  20907  neiflim  20924  supnfcls  20970  fclscf  20975  flimfnfcls  20978  tsmsfbas  21077  utopbas  21185  xpsxmet  21330  xpsdsval  21331  xpsmet  21332  tmsxms  21436  tmsms  21437  imasf1oxms  21439  imasf1oms  21440  prdsxms  21480  prdsms  21481  tmsxpsval  21488  retopbas  21716  cnngp  21735  cnperf  21773  retopcon  21782  fsumcn  21837  abscncf  21868  recncf  21869  imcncf  21870  cjcncf  21871  mulc1cncf  21872  cncfcn1  21877  cncfmpt2f  21881  cncfmpt2ss  21882  addccncf  21883  cdivcncf  21884  negcncf  21885  negfcncf  21886  abscncfALT  21887  cnmpt2pc  21891  xrhmeo  21909  oprpiece1res1  21914  oprpiece1res2  21915  cnrehmeo  21916  iscau3  22183  caubl  22212  caublcls  22213  rrxcph  22286  rrxmval  22294  rrxdstprj1  22298  evthicc2  22346  ovolre  22414  volsuplem  22443  uniiccdif  22470  uniioovol  22471  uniiccvol  22472  uniioombllem3  22478  uniioombllem4  22479  uniioombllem5  22480  dyadmbllem  22492  volcn  22499  volivth  22500  itgfsum  22719  iblabslem  22720  iblabs  22721  bddmulibl  22731  cnlimc  22778  cnlimci  22779  dvres3  22803  dvres3a  22804  dvidlem  22805  dvcnp2  22809  dvcn  22810  dvnadd  22818  dvnres  22820  cpnord  22824  cpnres  22826  dvaddbr  22827  dvmulbr  22828  dvcmul  22833  dvcmulf  22834  dvcobr  22835  dvcjbr  22838  dvrec  22844  dvmptntr  22860  dvmptfsum  22862  dveflem  22866  dvef  22867  rolle  22877  dvlipcn  22881  c1liplem1  22883  dvgt0lem2  22890  dvivth  22897  lhop1lem  22900  dvfsumabs  22910  ftc1a  22924  ftc1cn  22930  ftc2  22931  deg1mul3le  23000  plyssc  23089  plyeq0  23100  coeeulem  23113  0dgr  23134  coemulc  23144  coe0  23145  coesub  23146  coe1termlem  23147  dgrmulc  23160  dgrsub  23161  dgrcolem1  23162  dgrcolem2  23163  dvnply2  23175  plycpn  23177  plyremlem  23192  fta1lem  23195  vieta1lem2  23199  aalioulem3  23225  dvntaylp  23261  taylthlem1  23263  taylthlem2  23264  ulmcn  23289  psercn  23316  pserdv  23319  abelth  23331  efcn  23333  efcvx  23339  pige3  23407  dvrelog  23517  logcn  23527  dvloglem  23528  dvlog  23531  dvlog2  23533  efopnlem2  23537  logccv  23543  cxpcn  23620  cxpcn2  23621  cxpcn3  23623  resqrtcn  23624  sqrtcn  23625  loglesqrt  23633  atancn  23797  rlimcnp3  23828  jensen  23849  lgamgulmlem2  23890  ftalem3  23934  basellem2  23943  dchrfi  24118  dchrisumlema  24261  pntrsumo1  24338  pntrsumbnd  24339  pntlem3  24382  cusgrasizeindslem2  25137  efghgrpOLD  26036  sspid  26299  ssps  26304  helch  26831  hhssnv  26850  hhsssh  26855  shintcl  26918  chintcl  26920  shlesb1i  26974  omlsi  26992  chlejb1i  27064  chm0i  27078  chabs1  27104  chabs2  27105  spanun  27133  cmidi  27198  pjidmcoi  27765  csmdsymi  27922  sumdmdlem2  28007  dmdbr5ati  28010  mdcompli  28017  dmdcompli  28018  disjdifprg  28124  fcoinver  28153  xppreima  28187  padct  28250  xrinfm  28276  xrinfmOLD  28277  clatp0cl  28377  clatp1cl  28378  xrsmulgzz  28384  xrsp0  28387  xrsp1  28388  gsumle  28486  gsummpt2co  28487  gsumvsca1  28490  gsumvsca2  28491  mdetpmtr1  28594  reff  28611  locfinreflem  28612  pnfneige0  28702  esumsnf  28830  esumcvg  28852  pwsiga  28897  sigagenid  28918  baselcarsg  29083  bnj1253  29771  cvmlift2lem6  29976  mrsubrn  30096  mrsubff1  30097  mrsub0  30099  mrsubccat  30101  mrsubcn  30102  elmrsubrn  30103  elmsubrn  30111  msubrn  30112  msubff1  30139  mthmpps  30165  trpredtr  30415  trpredpo  30420  wzel  30451  frrlem5c  30464  frrlem10  30469  imagesset  30662  ivthALT  30933  fness  30947  fneref  30948  refssfne  30956  fnemeet1  30964  fnejoin2  30967  filnetlem2  30977  filnetlem4  30979  ontgval  31033  bj-rabtr  31439  bj-rabtrAUTO  31441  elxp8  31675  mblfinlem3  31880  mblfinlem4  31881  ismblfin  31882  ovoliunnfl  31883  voliunnfl  31885  volsupnfl  31886  mbfposadd  31889  ftc1cnnclem  31916  ftc1cnnc  31917  ftc1anc  31926  ftc2nc  31927  areacirclem2  31934  areacirclem3  31935  areacirclem4  31936  areacirc  31938  welb  31964  caures  31990  constcncf  31992  idcncf  31993  sub1cncf  31994  sub2cncf  31995  cnresima  31997  rngoidl  32158  atpsubN  33224  pol1N  33381  1psubclN  33415  cdlemefrs32fva  33873  dia2dimlem13  34550  dibord  34633  dochvalr  34831  hdmapevec  35312  ismrcd1  35446  ismrc  35449  incssnn0  35459  mzpclall  35475  rmydioph  35776  rmxdioph  35778  expdiophlem2  35784  expdioph  35785  aomclem6  35824  kelac1  35828  gicabl  35864  rgspnid  35945  itgpowd  36006  arearect  36007  areaquad  36008  clcnvlem  36137  cnvtrucl0  36138  cnvtrcl0  36140  fvilbd  36188  relexp0a  36215  brfvrtrcld  36233  corcltrcl  36238  wnefimgd  36507  wfximgfd  36512  extoimad  36514  funfvima2d  36519  nzss  36573  lhe4.4ex1a  36585  dvsconst  36586  dvsid  36587  dvsef  36588  dvconstbi  36590  binomcxplemnn0  36605  onfrALTlem3  36817  onfrALTlem3VD  37194  cnopn  37285  unisn0  37304  founiiun  37344  founiiun0  37363  evthiccabs  37479  islptre  37576  cncfshift  37628  addccncf2  37630  fsumcncf  37632  cncfperiod  37633  negcncfg  37635  cncfcompt  37637  ioccncflimc  37640  cncfuni  37641  icccncfext  37642  cncficcgt0  37643  icocncflimc  37644  cncfiooicclem1  37648  cncfiooicc  37649  cncfiooiccre  37650  cxpcncf2  37655  fprodcncf  37656  dvcosre  37658  dvcnre  37663  fperdvper  37667  dvmptresicc  37668  dvmptfprod  37697  itgsinexplem1  37707  itgcoscmulx  37723  ibliooicc  37725  itgsincmulx  37728  itgsubsticclem  37729  itgiccshift  37734  itgperiod  37735  itgsbtaddcnst  37736  dirkeritg  37841  dirkercncflem2  37843  dirkercncflem4  37845  fourierdlem16  37862  fourierdlem18  37864  fourierdlem21  37867  fourierdlem22  37868  fourierdlem23  37869  fourierdlem32  37879  fourierdlem33  37880  fourierdlem39  37886  fourierdlem40  37887  fourierdlem57  37904  fourierdlem58  37905  fourierdlem59  37906  fourierdlem62  37909  fourierdlem68  37915  fourierdlem72  37919  fourierdlem73  37920  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem78  37925  fourierdlem83  37930  fourierdlem84  37931  fourierdlem85  37932  fourierdlem88  37935  fourierdlem93  37940  fourierdlem94  37941  fourierdlem95  37942  fourierdlem97  37944  fourierdlem101  37948  fourierdlem103  37950  fourierdlem104  37951  fourierdlem111  37958  fourierdlem112  37959  fourierdlem113  37960  sqwvfoura  37969  sqwvfourb  37970  fouriersw  37972  fouriercn  37973  etransclem18  37994  etransclem22  37998  etransclem34  38010  etransclem46  38022  etransclem47  38023  sge0fsum  38074  hoidmvlelem2  38259  funresfunco  38434  uhgrsubgrself  39083  uhgrspansubgr  39094  nbupgr  39142  nbumgrvtx  39144  nbgr2vtx1edg  39148  cusgrexi  39229  submgmid  39378  rnghmsscmap2  39560  rhmsscmap2  39606  srhmsubc  39663  fldhmsubc  39671  srhmsubcALTV  39682  fldhmsubcALTV  39690  elbigolo1  39955
  Copyright terms: Public domain W3C validator