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

Theorem ssid 3523
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 3508 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  eqimssi  3558  eqimss2i  3559  nsspssun  3731  inv1  3812  disjpss  3877  difid  3895  pwidg  4023  elssuni  4275  unimax  4281  intmin  4302  rintn0  4416  sseliALT  4578  ordunidif  4926  xpss1  5109  xpss2  5110  residm  5303  resdm  5313  resmpt3  5322  ssrnres  5443  dffn3  5736  fdmrn  5744  fvreseq1  5980  fimacnv  6011  iunpw  6592  onsucuni  6641  tfisi  6671  fparlem3  6882  fparlem4  6883  funsssuppss  6923  suppofss1d  6934  suppofss2d  6935  tfrlem1  7042  tz7.48-2  7104  oaordi  7192  omwordi  7217  omass  7226  nnaordi  7264  nnmwordi  7281  fpmg  7441  ralxpmap  7465  boxcutc  7509  domss2  7673  0fin  7744  en1eqsn  7746  findcard2d  7758  fimax2g  7762  domunfican  7789  pwfi  7811  fissuni  7821  fipreima  7822  fsuppmptif  7855  fsuppco2  7858  fsuppcor  7859  mapfienlem1  7860  mapfienlem2  7861  wofib  7966  wemapso  7972  sucprcregOLD  8022  noinfep  8072  noinfepOLD  8073  cantnfval2  8084  cantnfp1lem3  8095  cantnflem1d  8103  cantnflem1  8104  cantnfval2OLD  8114  cantnfp1lem3OLD  8121  tcidm  8173  tc0  8174  r1rankidb  8218  r1pw  8259  rankr1id  8276  scott0  8300  htalem  8310  xpomen  8389  infpwfien  8439  alephsmo  8479  dfac12lem3  8521  ackbij2lem4  8618  cflem  8622  cflecard  8629  cflim2  8639  cfslb  8642  fin4en1  8685  fin23lem13  8708  fin23lem15  8710  fin23lem36  8724  isf32lem1  8729  fin67  8771  dcomex  8823  zorn2lem4  8875  alephexp2  8952  fpwwe2lem13  9016  canthnumlem  9022  wunex2  9112  wuncidm  9120  eltsk2g  9125  axgroth6  9202  axgroth3  9205  xrsup  11959  expcl  12148  hashcard  12391  hashf1lem2  12467  lo1eq  13350  rlimeq  13351  serclim0  13359  isercolllem2  13447  isercoll  13449  summolem3  13495  isum  13500  fsumser  13511  fsumcl  13514  fsum2d  13545  fsumabs  13574  fsumrlim  13584  fsumo1  13585  fsumiun  13594  flo1  13625  eflt  13709  xpnnenOLD  13800  rpnnen2lem3  13807  rpnnen2lem5  13809  rpnnen2lem11  13815  rpnnen2  13816  rexpen  13818  eulerthlem2  14167  ressid  14546  ressinbas  14547  mremre  14855  yon11  15387  yon12  15388  yon2  15389  yonpropd  15391  oppcyon  15392  yonffth  15407  oduclatb  15627  ipopos  15643  fpwipodrs  15647  submid  15792  mulgnncl  15957  mulgnn0cl  15958  mulgcl  15959  subgid  15998  cntrnsg  16174  symggen  16291  sylow3lem5  16447  lsmss1  16480  lsmss2  16482  gsumzres  16705  gsumzcl2  16706  gsumzf1o  16708  gsumzresOLD  16709  gsumzclOLD  16710  gsumzf1oOLD  16711  gsumadd  16729  gsumaddOLD  16730  gsumzsplitOLD  16736  gsumzmhm  16748  gsumzmhmOLD  16749  gsumzoppg  16758  gsumzoppgOLD  16759  gsumzinvOLD  16761  gsumsubOLD  16766  gsum2dlem1  16788  gsum2dlem2  16789  gsum2d  16790  gsum2dOLD  16791  dprdfinv  16849  dprdfinvOLD  16856  dprdf1  16870  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  dprd2db  16882  dpjidcl  16897  dpjidclOLD  16904  ablfac1eulem  16913  ablfac1eu  16914  ablfaclem2  16927  gsumdixpOLD  17041  gsumdixp  17042  subrgid  17214  lcomfsupOLD  17332  lcomfsupp  17333  lss1  17368  lbsextlem1  17587  rlmval2  17623  rlmbas  17624  rlmplusg  17625  rlm0  17626  rlmmulr  17628  rlmsca  17629  rlmsca2  17630  rlmvsca  17631  rlmtopn  17632  rlmds  17633  psrass1lem  17800  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  mplsubrglem  17871  mplsubrglemOLD  17872  mplcoe1  17898  mplcoe5  17902  mplbas2  17905  mplbas2OLD  17906  evlslem4OLD  17944  evlslem4  17945  psrbagev1  17948  psrbagev1OLD  17949  evlslem2  17951  ply1coeOLD  18109  znf1o  18357  zntoslem  18362  regsumsupp  18425  css0  18487  frlmip  18576  uvcresum  18591  frlmsslsp  18596  frlmsslspOLD  18597  frlmlbs  18598  frlmup1  18599  mamures  18659  mdetrsca2  18873  mdetrlin2  18876  mdetunilem5  18885  mdetunilem9  18889  smadiadetglem1  18940  smadiadetglem2  18941  pmatcollpw3  19052  cpmadumatpolylem2  19150  topopn  19182  fiinbas  19220  topbas  19240  topcld  19302  clstop  19336  ntrtop  19337  opnneissb  19381  opnssneib  19382  opnneiid  19393  neiptopuni  19397  neiptoptop  19398  maxlp  19414  isperf2  19419  restopn2  19444  restperf  19451  idcn  19524  cnconst2  19550  lmres  19567  rncmp  19662  fiuncmp  19670  cmpfi  19674  concn  19693  1stcelcls  19728  llyidm  19755  nllyidm  19756  toplly  19757  kgentopon  19774  kgencn2  19793  ptpjpre1  19807  ptbasfi  19817  ptcld  19849  xkopt  19891  elqtop2  19937  qtopuni  19938  ptcmpfi  20049  fbssfi  20073  opnfbas  20078  filtop  20091  isfil2  20092  isfild  20094  fsubbas  20103  ssfg  20108  filssufilg  20147  ufileu  20155  imaelfm  20187  rnelfm  20189  fmfnfmlem4  20193  neiflim  20210  supnfcls  20256  fclscf  20261  flimfnfcls  20264  tsmsfbas  20361  utopbas  20473  xpsxmet  20618  xpsdsval  20619  xpsmet  20620  tmsxms  20724  tmsms  20725  imasf1oxms  20727  imasf1oms  20728  prdsxms  20768  prdsms  20769  tmsxpsval  20776  retopbas  21002  cnngp  21022  cnperf  21060  retopcon  21069  fsumcn  21109  abscncf  21140  recncf  21141  imcncf  21142  cjcncf  21143  mulc1cncf  21144  cncfcn1  21149  cncfmpt2f  21153  cncfmpt2ss  21154  addccncf  21155  cdivcncf  21156  negcncf  21157  negfcncf  21158  abscncfALT  21159  cnmpt2pc  21163  xrhmeo  21181  oprpiece1res1  21186  oprpiece1res2  21187  cnrehmeo  21188  iscau3  21452  caubl  21481  caublcls  21482  rrxip  21557  rrxcph  21559  rrxmval  21567  rrxdstprj1  21571  evthicc2  21607  ovolre  21671  volsuplem  21700  uniiccdif  21722  uniioovol  21723  uniiccvol  21724  uniioombllem3  21729  uniioombllem4  21730  uniioombllem5  21731  dyadmbllem  21743  volcn  21750  volivth  21751  itgfsum  21968  iblabslem  21969  iblabs  21970  bddmulibl  21980  cnlimc  22027  cnlimci  22028  dvres3  22052  dvres3a  22053  dvidlem  22054  dvcnp2  22058  dvcn  22059  dvnadd  22067  dvnres  22069  cpnord  22073  cpnres  22075  dvaddbr  22076  dvmulbr  22077  dvcmul  22082  dvcmulf  22083  dvcobr  22084  dvcjbr  22087  dvrec  22093  dvmptntr  22109  dvmptfsum  22111  dveflem  22115  dvef  22116  rolle  22126  dvlipcn  22130  c1liplem1  22132  dvgt0lem2  22139  dvivth  22146  lhop1lem  22149  dvfsumabs  22159  ftc1a  22173  ftc1cn  22179  ftc2  22180  deg1mul3le  22252  plyssc  22332  plyeq0  22343  coeeulem  22356  0dgr  22377  coemulc  22386  coe0  22387  coesub  22388  coe1termlem  22389  dgrmulc  22402  dgrsub  22403  dgrcolem1  22404  dgrcolem2  22405  dvnply2  22417  plycpn  22419  plyremlem  22434  fta1lem  22437  vieta1lem2  22441  aalioulem3  22464  dvntaylp  22500  taylthlem1  22502  taylthlem2  22503  ulmcn  22528  psercn  22555  pserdv  22558  abelth  22570  efcn  22572  efcvx  22578  pige3  22643  dvrelog  22746  logcn  22756  dvloglem  22757  dvlog  22760  dvlog2  22762  efopnlem2  22766  logccv  22772  cxpcn  22847  cxpcn2  22848  cxpcn3  22850  resqrtcn  22851  sqrtcn  22852  loglesqrt  22860  atancn  22995  rlimcnp3  23025  jensen  23046  ftalem3  23076  basellem2  23083  dchrfi  23258  dchrisumlema  23401  pntrsumo1  23478  pntrsumbnd  23479  pntlem3  23522  cusgrasizeindslem2  24150  efghgrp  25051  sspid  25314  ssps  25319  helch  25837  hhssnv  25856  hhsssh  25861  shintcl  25924  chintcl  25926  shlesb1i  25980  omlsi  25998  chlejb1i  26070  chm0i  26084  chabs1  26110  chabs2  26111  spanun  26139  cmidi  26204  pjidmcoi  26772  csmdsymi  26929  sumdmdlem2  27014  dmdbr5ati  27017  mdcompli  27024  dmdcompli  27025  disjdifprg  27109  fcoinver  27133  xppreima  27159  xrinfm  27243  clatp0cl  27321  clatp1cl  27322  xrsmulgzz  27328  xrsp0  27331  xrsp1  27332  gsumle  27433  gsummpt2co  27434  gsumvsca1  27436  gsumvsca2  27437  pnfneige0  27569  esumsn  27712  esumcvg  27732  pwsiga  27770  sigagenid  27791  lgamgulmlem2  28212  cvmlift2lem6  28393  relexpdm  28533  relexprn  28534  rtrclreclem.refl  28542  rtrclreclem.subset  28543  prodmolem3  28642  iprod  28647  iprodn0  28649  fprodss  28657  fprodcl  28661  fprod2d  28688  risefaccl  28714  fallfaccl  28715  trpredtr  28890  trpredpo  28895  wzel  28957  frrlem5c  28970  frrlem10  28975  imagesset  29180  ontgval  29473  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  mbfposadd  29639  ftc1cnnclem  29665  ftc1cnnc  29666  ftc1anc  29675  ftc2nc  29676  areacirclem2  29685  areacirclem3  29686  areacirclem4  29687  areacirc  29689  ivthALT  29730  fness  29754  ssref  29755  fneref  29756  refref  29757  refssfne  29766  fnemeet1  29787  fnejoin2  29790  filnetlem2  29800  filnetlem4  29802  welb  29830  caures  29856  constcncf  29858  idcncf  29859  sub1cncf  29860  sub2cncf  29861  cnresima  29863  rngoidl  30024  ismrcd1  30234  ismrc  30237  incssnn0  30247  mzpclall  30263  rmydioph  30560  rmxdioph  30562  expdiophlem2  30568  expdioph  30569  aomclem6  30609  kelac1  30613  gicabl  30651  rgspnid  30726  itgpowd  30787  arearect  30788  areaquad  30789  nzss  30822  lhe4.4ex1a  30834  dvsconst  30835  dvsid  30836  dvsef  30837  dvconstbi  30839  cnopn  31018  evthiccabs  31093  islptre  31161  cncfshift  31212  addccncf2  31214  fsumcncf  31216  cncfperiod  31217  negcncfg  31219  cncfcompt  31221  ioccncflimc  31224  cncfuni  31225  icccncfext  31226  cncficcgt0  31227  icocncflimc  31228  cncfiooicclem1  31232  cncfiooicc  31233  cncfiooiccre  31234  dvcosre  31239  dvcnre  31244  fperdvper  31248  dvmptresicc  31249  dvasinbx  31250  itgsinexplem1  31271  itgcoscmulx  31287  ibliooicc  31289  itgsincmulx  31292  itgsubsticclem  31293  iblcncfioo  31296  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem16  31423  fourierdlem18  31425  fourierdlem21  31428  fourierdlem22  31429  fourierdlem23  31430  fourierdlem32  31439  fourierdlem33  31440  fourierdlem39  31446  fourierdlem40  31447  fourierdlem57  31464  fourierdlem58  31465  fourierdlem59  31466  fourierdlem62  31469  fourierdlem68  31475  fourierdlem72  31479  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem83  31490  fourierdlem84  31491  fourierdlem85  31492  fourierdlem88  31495  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem93  31500  fourierdlem94  31501  fourierdlem95  31502  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  fouriercn  31533  funresfunco  31677  onfrALTlem3  32396  onfrALTlem3VD  32767  bnj1253  33152  bj-rabtr  33578  bj-rabtrAUTO  33580  atpsubN  34549  pol1N  34706  1psubclN  34740  cdlemefrs32fva  35196  dia2dimlem13  35873  dibord  35956  dochvalr  36154  hdmapevec  36635  xptrrel  36785
  Copyright terms: Public domain W3C validator