Theorem ssid 3956

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901

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

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

This theorem is referenced by:  ssidd  3957  eqimssd  3990  eqimsscd  3991  eqimssi  3994  eqimss2i  3995  nsspssun  4220  difidALT  4329  inv1  4350  disjpss  4413  pwidg  4574  elssuni  4894  unimax  4900  intmin  4923  rintn0  5064  sseliALT  5254  inxpssres  5641  xpss1  5643  xpss2  5644  residm  5969  resdm  5985  resmpt3  5997  cnvrescnv  6153  onelssex  6366  ordunidif  6367  funresfunco  6533  dffn3  6674  fdmrn  6693  fvreseq1  6984  iunpw  7716  onsucuni  7770  tfisi  7801  fparlem3  8056  fparlem4  8057  funsssuppss  8132  tfrlem1  8307  tz7.48-2  8373  oaordi  8473  omwordi  8498  omass  8507  nnaordi  8546  nnmwordi  8563  naddunif  8621  fpmg  8806  boxcutc  8879  domss2  9064  findcard2d  9091  fimax2g  9186  domunfican  9222  fipreima  9258  fimin2g  9402  wofib  9450  wemapso  9456  noinfep  9569  cantnfval2  9578  tcidm  9653  tc0  9654  r1rankidb  9716  r1pw  9757  rankr1id  9774  scott0  9798  xpomen  9925  infpwfien  9972  alephsmo  10012  dfac12lem3  10056  cflem  10155  cflemOLD  10156  cflecard  10163  cfslb  10176  fin4en1  10219  fin23lem13  10242  fin23lem36  10258  isf32lem1  10263  fin67  10305  dcomex  10357  zorn2lem4  10409  alephexp2  10492  fpwwe2lem12  10553  canthnumlem  10559  wuncidm  10657  eltsk2g  10662  axgroth6  10739  axgroth3  10742  xrsup  13788  expcl  14002  hashcard  14278  hashf1lem2  14379  xptrrel  14903  cotrtrclfv  14935  rtrclreclem2  14982  lo1eq  15491  rlimeq  15492  serclim0  15500  isercolllem2  15589  isercoll  15591  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  fprod2d  15904  risefaccl  15938  fallfaccl  15939  eflt  16042  rpnnen2lem3  16141  rpnnen2lem5  16143  rpnnen2lem12  16150  rexpen  16153  ressbasssg  17164  ressid  17171  ressinbas  17172  oduclatb  18430  ipopos  18459  fpwipodrs  18463  ghmghmrn  19164  elcntr  19259  cntrnsg  19273  0symgefmndeq  19323  sylow3lem5  19560  lsmss1  19594  lsmss2  19596  cmnbascntr  19734  cntrcmnd  19771  cntrabl  19772  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumadd  19852  gsumzmhm  19866  gsumzoppg  19873  dprdf1  19964  ablfac1eulem  20003  gsumle  20074  subrgid  20506  srhmsubc  20613  lbsextlem1  21113  rlmval2  21144  znf1o  21506  zntoslem  21511  css0  21644  uvcresum  21748  frlmlbs  21752  psrass1lem  21888  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  mdetunilem9  22564  smadiadetglem1  22615  smadiadetglem2  22616  pmatcollpw3  22728  topopn  22850  fiinbas  22896  topbas  22916  topcld  22979  ntrtop  23014  opnneissb  23058  opnssneib  23059  opnneiid  23070  maxlp  23091  isperf2  23096  restperf  23128  idcn  23201  cnconst2  23227  lmres  23244  fiuncmp  23348  1stcelcls  23405  ssref  23456  refref  23457  kgencn2  23501  ptpjpre1  23515  ptbasfi  23525  xkopt  23599  elqtop2  23645  ptcmpfi  23757  fbssfi  23781  opnfbas  23786  filtop  23799  isfil2  23800  isfild  23802  fsubbas  23811  ssfg  23816  filssufilg  23855  ufileu  23863  imaelfm  23895  rnelfm  23897  fmfnfmlem4  23901  neiflim  23918  fclscf  23969  flimfnfcls  23972  tsmsfbas  24072  xpsxmet  24324  xpsdsval  24325  xpsmet  24326  tmsxms  24430  tmsms  24431  imasf1oxms  24433  imasf1oms  24434  prdsxms  24474  prdsms  24475  tmsxpsval  24482  retopbas  24704  cnngp  24723  cnopn  24730  cnperf  24765  retopconn  24774  fsumcn  24817  abscncf  24850  recncf  24851  imcncf  24852  cjcncf  24853  mulc1cncf  24854  cncfcn1  24860  cncfmpt2f  24864  cncfmpt2ss  24865  addccncf  24866  idcncf  24867  sub1cncf  24868  sub2cncf  24869  cdivcncf  24870  negcncf  24871  negcncfOLD  24872  negfcncf  24873  abscncfALT  24874  cnmpopc  24878  xrhmeo  24900  oprpiece1res1  24905  oprpiece1res2  24906  cnrehmeo  24907  cnrehmeoOLD  24908  iscau3  25234  caubl  25264  caublcls  25265  mulcncf  25402  evthicc2  25417  ovolre  25482  volsuplem  25512  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  dyadmbllem  25556  volivth  25564  itgfsum  25784  iblabslem  25785  iblabs  25786  bddmulibl  25796  cnlimc  25845  cnlimci  25846  dvcnp2  25877  dvcnp2OLD  25878  dvcn  25879  cpnord  25893  cpnres  25895  dvmptntr  25931  dvmptfsum  25935  rolle  25950  dvlipcn  25955  c1liplem1  25957  dvivth  25971  dvfsumabs  25985  ftc1a  26000  ftc1cn  26006  plyssc  26161  plyeq0  26172  0dgr  26206  coemulc  26216  coe0  26217  coesub  26218  coe1termlem  26219  dgrmulc  26233  dgrsub  26234  dvnply2  26251  plycpn  26253  plyremlem  26268  fta1lem  26271  vieta1lem2  26275  aalioulem3  26298  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmcn  26364  psercn  26392  abelth  26407  efcn  26409  efcvx  26415  dvrelog  26602  logcn  26612  dvloglem  26613  dvlog  26616  dvlog2  26618  efopnlem2  26622  logccv  26628  cxpcn  26710  cxpcnOLD  26711  cxpcn3  26714  resqrtcn  26715  sqrtcn  26716  loglesqrt  26727  atancn  26902  jensen  26955  ftalem3  27041  dchrfi  27222  dchrisumlema  27455  pntlem3  27576  madebday  27896  expscl  28427  bdaypw2n0bndlem  28459  uhgrsubgrself  29353  uhgrspansubgr  29364  umgr2adedgwlk  30018  umgr2adedgwlkon  30019  umgr2adedgspth  30021  upgr1wlkdlem2  30221  sspid  30800  ssps  30805  helch  31318  hhssnv  31339  hhsssh  31344  shintcl  31405  chintcl  31407  shlesb1i  31461  omlsi  31479  chlejb1i  31551  chm0i  31565  chabs1  31591  chabs2  31592  spanun  31620  cmidi  31685  pjidmcoi  32252  csmdsymi  32409  sumdmdlem2  32494  dmdbr5ati  32497  mdcompli  32504  dmdcompli  32505  disjdifprg  32650  fcoinver  32679  f1rnen  32706  xppreima  32723  padct  32797  xrinfm  32835  indconst1  32940  clatp0cl  33058  clatp1cl  33059  xrsp0  33094  xrsp1  33095  cntrcrng  33163  cycpmconjslem1  33236  cycpmconjslem2  33237  gsumvsca1  33308  gsumvsca2  33309  qusxpid  33444  ellspds  33449  rspidlid  33456  rlmdim  33766  reff  33996  locfinreflem  33997  esumsnf  34221  esumcvg  34243  sigagenid  34308  iblidicc  34749  cxpcncf1  34752  fdvposlt  34756  fdvneggt  34757  fdvposle  34758  fdvnegge  34759  logdivsqrle  34807  bnj1253  35173  fineqvac  35272  fineqvnttrclse  35280  noinfepfnregs  35288  cvmlift2lem6  35502  satfun  35605  mrsubrn  35707  elmrsubrn  35714  elmsubrn  35722  msubrn  35723  imagesset  36147  ivthALT  36529  fness  36543  fneref  36544  refssfne  36552  fnemeet1  36560  fnejoin2  36563  filnetlem2  36573  filnetlem4  36575  ontgval  36625  knoppcnlem10  36702  knoppcnlem11  36703  bj-rabtr  37131  bj-rabtrAUTO  37133  bj-disj2r  37229  bj-restsnid  37288  bj-resta  37297  bj-imdirco  37391  elxp8  37572  finorwe  37583  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  mbfposadd  37864  ftc1cnnclem  37888  ftc1cnnc  37889  ftc1anc  37898  ftc2nc  37899  areacirclem2  37906  areacirclem4  37908  areacirc  37910  caures  37957  constcncf  37959  brssrid  38751  brcnvssrid  38756  refrelid  38771  n0eldmqs  38902  atpsubN  40009  pol1N  40166  dia2dimlem13  41332  dibord  41415  dochvalr  41613  hdmapevec  42091  lcmineqlem10  42288  lcmineqlem12  42290  ismrcd1  42936  ismrc  42939  incssnn0  42949  mzpclall  42965  rmydioph  43252  rmxdioph  43254  expdiophlem2  43260  expdioph  43261  aomclem6  43297  kelac1  43301  gicabl  43337  arearect  43453  areaquad  43454  unielid  43457  oege2  43545  oacl2g  43568  ofoaf  43593  clcnvlem  43860  cnvtrcl0  43863  fvilbd  43926  relexp0a  43953  corcltrcl  43976  clsk1indlem2  44279  ntrclskb  44306  wnefimgd  44398  mnuprdlem4  44512  nzss  44554  lhe4.4ex1a  44566  dvsconst  44567  dvsid  44568  dvsef  44569  binomcxplemnn0  44586  onfrALTlem3  44781  onfrALTlem3VD  45123  unisn0  45295  founiiun0  45430  evthiccabs  45738  climconstmpt  45898  cncfshift  46114  addccncf2  46116  cncfcompt  46123  ioccncflimc  46125  icocncflimc  46129  cncfiooicclem1  46133  cncfiooicc  46134  cncfiooiccre  46135  cxpcncf2  46139  add1cncf  46141  add2cncf  46142  sub1cncfd  46143  sub2cncfd  46144  dvcosre  46152  dvmptfprod  46185  ibliooicc  46211  itgsincmulx  46214  itgsubsticclem  46215  itgiccshift  46220  itgperiod  46221  itgsbtaddcnst  46222  dirkeritg  46342  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem16  46363  fourierdlem18  46365  fourierdlem21  46368  fourierdlem22  46369  fourierdlem23  46370  fourierdlem32  46379  fourierdlem33  46380  fourierdlem39  46386  fourierdlem40  46387  fourierdlem57  46403  fourierdlem58  46404  fourierdlem59  46405  fourierdlem62  46408  fourierdlem68  46414  fourierdlem72  46418  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem78  46424  fourierdlem83  46429  fourierdlem84  46430  fourierdlem85  46431  fourierdlem88  46434  fourierdlem93  46439  fourierdlem94  46440  fourierdlem95  46441  fourierdlem97  46443  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem112  46458  fourierdlem113  46459  sqwvfoura  46468  sqwvfourb  46469  fouriersw  46471  fouriercn  46472  etransclem18  46492  etransclem22  46496  etransclem34  46508  etransclem46  46520  etransclem47  46521  sge0fsum  46627  meaiininclem  46726  hoidmvlelem2  46836  hspdifhsp  46856  hspmbllem2  46867  hspmbl  46869  iinhoiicclem  46913  pimgtmnf2  46954  smflimsuplem1  47060  smflimsuplem6  47065  cjnpoly  47131  srhmsubcALTV  48567  imaidfu2lem  49350  imaidfu  49351  imaidfu2  49352  setc1onsubc  49843