Theorem ssid 4006

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	⊢ 𝐴 ⊆ 𝐴

Proof of Theorem ssid

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
2	1	ssriv 3987	1 ⊢ 𝐴 ⊆ 𝐴

Syntax hints:   ∈ wcel 2108   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795

This theorem depends on definitions:  df-bi 207  df-ss 3968

This theorem is referenced by:  ssidd  4007  eqimssd  4040  eqimsscd  4041  eqimssi  4044  eqimss2i  4045  nsspssun  4268  difidALT  4377  inv1  4398  disjpss  4461  pwidg  4620  elssuni  4937  unimax  4944  intmin  4968  rintn0  5109  sseliALT  5309  inxpssres  5702  xpss1  5704  xpss2  5705  residm  6028  resdm  6044  resmpt3  6056  cnvrescnv  6215  onelssex  6432  ordunidif  6433  funresfunco  6607  dffn3  6748  fdmrn  6767  fvreseq1  7059  iunpw  7791  onsucuni  7848  tfisi  7880  fparlem3  8139  fparlem4  8140  funsssuppss  8215  tfrlem1  8416  tz7.48-2  8482  oaordi  8584  omwordi  8609  omass  8618  nnaordi  8656  nnmwordi  8673  naddunif  8731  fpmg  8908  boxcutc  8981  domss2  9176  findcard2d  9206  0finOLD  9210  en1eqsnOLD  9309  fimax2g  9322  domunfican  9361  fipreima  9398  fimin2g  9537  wofib  9585  wemapso  9591  noinfep  9700  cantnfval2  9709  tcidm  9786  tc0  9787  r1rankidb  9844  r1pw  9885  rankr1id  9902  scott0  9926  xpomen  10055  infpwfien  10102  alephsmo  10142  dfac12lem3  10186  cflem  10285  cflemOLD  10286  cflecard  10293  cfslb  10306  fin4en1  10349  fin23lem13  10372  fin23lem36  10388  isf32lem1  10393  fin67  10435  dcomex  10487  zorn2lem4  10539  alephexp2  10621  fpwwe2lem12  10682  canthnumlem  10688  wuncidm  10786  eltsk2g  10791  axgroth6  10868  axgroth3  10871  xrsup  13908  expcl  14120  hashcard  14394  hashf1lem2  14495  xptrrel  15019  cotrtrclfv  15051  rtrclreclem2  15098  lo1eq  15604  rlimeq  15605  serclim0  15613  isercolllem2  15702  isercoll  15704  fsum2d  15807  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  fprod2d  16017  risefaccl  16051  fallfaccl  16052  eflt  16153  rpnnen2lem3  16252  rpnnen2lem5  16254  rpnnen2lem12  16261  rexpen  16264  ressbasssg  17282  ressid  17290  ressinbas  17291  oduclatb  18552  ipopos  18581  fpwipodrs  18585  ghmghmrn  19253  elcntr  19348  cntrnsg  19362  0symgefmndeq  19411  sylow3lem5  19649  lsmss1  19683  lsmss2  19685  cmnbascntr  19823  cntrcmnd  19860  cntrabl  19861  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumadd  19941  gsumzmhm  19955  gsumzoppg  19962  dprdf1  20053  ablfac1eulem  20092  subrgid  20573  srhmsubc  20680  lbsextlem1  21160  rlmval2  21199  znf1o  21570  zntoslem  21575  css0  21707  uvcresum  21813  frlmlbs  21817  psrass1lem  21952  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  mdetunilem9  22626  smadiadetglem1  22677  smadiadetglem2  22678  pmatcollpw3  22790  topopn  22912  fiinbas  22959  topbas  22979  topcld  23043  ntrtop  23078  opnneissb  23122  opnssneib  23123  opnneiid  23134  maxlp  23155  isperf2  23160  restperf  23192  idcn  23265  cnconst2  23291  lmres  23308  fiuncmp  23412  1stcelcls  23469  ssref  23520  refref  23521  kgencn2  23565  ptpjpre1  23579  ptbasfi  23589  xkopt  23663  elqtop2  23709  ptcmpfi  23821  fbssfi  23845  opnfbas  23850  filtop  23863  isfil2  23864  isfild  23866  fsubbas  23875  ssfg  23880  filssufilg  23919  ufileu  23927  imaelfm  23959  rnelfm  23961  fmfnfmlem4  23965  neiflim  23982  fclscf  24033  flimfnfcls  24036  tsmsfbas  24136  xpsxmet  24390  xpsdsval  24391  xpsmet  24392  tmsxms  24499  tmsms  24500  imasf1oxms  24502  imasf1oms  24503  prdsxms  24543  prdsms  24544  tmsxpsval  24551  retopbas  24781  cnngp  24800  cnopn  24807  cnperf  24842  retopconn  24851  fsumcn  24894  abscncf  24927  recncf  24928  imcncf  24929  cjcncf  24930  mulc1cncf  24931  cncfcn1  24937  cncfmpt2f  24941  cncfmpt2ss  24942  addccncf  24943  idcncf  24944  sub1cncf  24945  sub2cncf  24946  cdivcncf  24947  negcncf  24948  negcncfOLD  24949  negfcncf  24950  abscncfALT  24951  cnmpopc  24955  xrhmeo  24977  oprpiece1res1  24982  oprpiece1res2  24983  cnrehmeo  24984  cnrehmeoOLD  24985  iscau3  25312  caubl  25342  caublcls  25343  mulcncf  25480  evthicc2  25495  ovolre  25560  volsuplem  25590  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  dyadmbllem  25634  volivth  25642  itgfsum  25862  iblabslem  25863  iblabs  25864  bddmulibl  25874  cnlimc  25923  cnlimci  25924  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  cpnord  25971  cpnres  25973  dvmptntr  26009  dvmptfsum  26013  rolle  26028  dvlipcn  26033  c1liplem1  26035  dvivth  26049  dvfsumabs  26063  ftc1a  26078  ftc1cn  26084  plyssc  26239  plyeq0  26250  0dgr  26284  coemulc  26294  coe0  26295  coesub  26296  coe1termlem  26297  dgrmulc  26311  dgrsub  26312  dvnply2  26329  plycpn  26331  plyremlem  26346  fta1lem  26349  vieta1lem2  26353  aalioulem3  26376  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmcn  26442  psercn  26470  abelth  26485  efcn  26487  efcvx  26493  dvrelog  26679  logcn  26689  dvloglem  26690  dvlog  26693  dvlog2  26695  efopnlem2  26699  logccv  26705  cxpcn  26787  cxpcnOLD  26788  cxpcn3  26791  resqrtcn  26792  sqrtcn  26793  loglesqrt  26804  atancn  26979  jensen  27032  ftalem3  27118  dchrfi  27299  dchrisumlema  27532  pntlem3  27653  madebday  27938  uhgrsubgrself  29297  uhgrspansubgr  29308  umgr2adedgwlk  29965  umgr2adedgwlkon  29966  umgr2adedgspth  29968  upgr1wlkdlem2  30165  sspid  30744  ssps  30749  helch  31262  hhssnv  31283  hhsssh  31288  shintcl  31349  chintcl  31351  shlesb1i  31405  omlsi  31423  chlejb1i  31495  chm0i  31509  chabs1  31535  chabs2  31536  spanun  31564  cmidi  31629  pjidmcoi  32196  csmdsymi  32353  sumdmdlem2  32438  dmdbr5ati  32441  mdcompli  32448  dmdcompli  32449  disjdifprg  32588  fcoinver  32617  f1rnen  32639  xppreima  32655  padct  32731  xrinfm  32758  clatp0cl  32966  clatp1cl  32967  xrsp0  33014  xrsp1  33015  cntrcrng  33073  gsumle  33101  cycpmconjslem1  33174  cycpmconjslem2  33175  gsumvsca1  33232  gsumvsca2  33233  qusxpid  33391  ellspds  33396  rspidlid  33403  rlmdim  33660  reff  33838  locfinreflem  33839  esumsnf  34065  esumcvg  34087  sigagenid  34152  iblidicc  34607  cxpcncf1  34610  fdvposlt  34614  fdvneggt  34615  fdvposle  34616  fdvnegge  34617  logdivsqrle  34665  bnj1253  35031  fineqvac  35111  cvmlift2lem6  35313  satfun  35416  mrsubrn  35518  elmrsubrn  35525  elmsubrn  35533  msubrn  35534  imagesset  35954  ivthALT  36336  fness  36350  fneref  36351  refssfne  36359  fnemeet1  36367  fnejoin2  36370  filnetlem2  36380  filnetlem4  36382  ontgval  36432  knoppcnlem10  36503  knoppcnlem11  36504  bj-rabtr  36931  bj-rabtrAUTO  36933  bj-disj2r  37029  bj-restsnid  37088  bj-resta  37097  bj-imdirco  37191  elxp8  37372  finorwe  37383  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfposadd  37674  ftc1cnnclem  37698  ftc1cnnc  37699  ftc1anc  37708  ftc2nc  37709  areacirclem2  37716  areacirclem4  37718  areacirc  37720  caures  37767  constcncf  37769  brssrid  38503  brcnvssrid  38508  refrelid  38523  n0eldmqs  38649  atpsubN  39755  pol1N  39912  dia2dimlem13  41078  dibord  41161  dochvalr  41359  hdmapevec  41837  lcmineqlem10  42039  lcmineqlem12  42041  ismrcd1  42709  ismrc  42712  incssnn0  42722  mzpclall  42738  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  aomclem6  43071  kelac1  43075  gicabl  43111  arearect  43227  areaquad  43228  unielid  43231  oege2  43320  oacl2g  43343  ofoaf  43368  clcnvlem  43636  cnvtrcl0  43639  fvilbd  43702  relexp0a  43729  corcltrcl  43752  clsk1indlem2  44055  ntrclskb  44082  wnefimgd  44174  mnuprdlem4  44294  nzss  44336  lhe4.4ex1a  44348  dvsconst  44349  dvsid  44350  dvsef  44351  binomcxplemnn0  44368  onfrALTlem3  44564  onfrALTlem3VD  44907  unisn0  45059  founiiun0  45195  evthiccabs  45509  climconstmpt  45673  cncfshift  45889  addccncf2  45891  cncfcompt  45898  ioccncflimc  45900  icocncflimc  45904  cncfiooicclem1  45908  cncfiooicc  45909  cncfiooiccre  45910  cxpcncf2  45914  add1cncf  45916  add2cncf  45917  sub1cncfd  45918  sub2cncfd  45919  dvcosre  45927  dvmptfprod  45960  ibliooicc  45986  itgsincmulx  45989  itgsubsticclem  45990  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem16  46138  fourierdlem18  46140  fourierdlem21  46143  fourierdlem22  46144  fourierdlem23  46145  fourierdlem32  46154  fourierdlem33  46155  fourierdlem39  46161  fourierdlem40  46162  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem62  46183  fourierdlem68  46189  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem83  46204  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem93  46214  fourierdlem94  46215  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  fouriercn  46247  etransclem18  46267  etransclem22  46271  etransclem34  46283  etransclem46  46295  etransclem47  46296  sge0fsum  46402  meaiininclem  46501  hoidmvlelem2  46611  hspdifhsp  46631  hspmbllem2  46642  hspmbl  46644  iinhoiicclem  46688  pimgtmnf2  46729  smflimsuplem1  46835  smflimsuplem6  46840  srhmsubcALTV  48241