Theorem ssid 4017

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3962

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

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

This theorem is referenced by:  ssidd  4018  eqimssd  4051  eqimsscd  4052  eqimssi  4055  eqimss2i  4056  nsspssun  4273  difidALT  4382  inv1  4403  disjpss  4466  pwidg  4624  elssuni  4941  unimax  4948  intmin  4972  rintn0  5113  sseliALT  5314  inxpssres  5705  xpss1  5707  xpss2  5708  residm  6029  resdm  6045  resmpt3  6057  cnvrescnv  6216  onelssex  6433  ordunidif  6434  funresfunco  6608  dffn3  6748  fdmrn  6767  fvreseq1  7058  iunpw  7789  onsucuni  7847  tfisi  7879  fparlem3  8137  fparlem4  8138  funsssuppss  8213  tfrlem1  8414  tz7.48-2  8480  oaordi  8582  omwordi  8607  omass  8616  nnaordi  8654  nnmwordi  8671  naddunif  8729  fpmg  8906  boxcutc  8979  domss2  9174  findcard2d  9204  0finOLD  9208  en1eqsnOLD  9306  fimax2g  9319  domunfican  9358  fipreima  9395  fimin2g  9534  wofib  9582  wemapso  9588  noinfep  9697  cantnfval2  9706  tcidm  9783  tc0  9784  r1rankidb  9841  r1pw  9882  rankr1id  9899  scott0  9923  xpomen  10052  infpwfien  10099  alephsmo  10139  dfac12lem3  10183  cflem  10282  cflemOLD  10283  cflecard  10290  cfslb  10303  fin4en1  10346  fin23lem13  10369  fin23lem36  10385  isf32lem1  10390  fin67  10432  dcomex  10484  zorn2lem4  10536  alephexp2  10618  fpwwe2lem12  10679  canthnumlem  10685  wuncidm  10783  eltsk2g  10788  axgroth6  10865  axgroth3  10868  xrsup  13904  expcl  14116  hashcard  14390  hashf1lem2  14491  xptrrel  15015  cotrtrclfv  15047  rtrclreclem2  15094  lo1eq  15600  rlimeq  15601  serclim0  15609  isercolllem2  15698  isercoll  15700  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  fprod2d  16013  risefaccl  16047  fallfaccl  16048  eflt  16149  rpnnen2lem3  16248  rpnnen2lem5  16250  rpnnen2lem12  16257  rexpen  16260  ressbasssg  17281  ressid  17289  ressinbas  17290  oduclatb  18564  ipopos  18593  fpwipodrs  18597  ghmghmrn  19265  elcntr  19360  cntrnsg  19374  0symgefmndeq  19425  sylow3lem5  19663  lsmss1  19697  lsmss2  19699  cmnbascntr  19837  cntrcmnd  19874  cntrabl  19875  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumadd  19955  gsumzmhm  19969  gsumzoppg  19976  dprdf1  20067  ablfac1eulem  20106  subrgid  20589  srhmsubc  20696  lbsextlem1  21177  rlmval2  21216  znf1o  21587  zntoslem  21592  css0  21724  uvcresum  21830  frlmlbs  21834  psrass1lem  21969  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  mdetunilem9  22641  smadiadetglem1  22692  smadiadetglem2  22693  pmatcollpw3  22805  topopn  22927  fiinbas  22974  topbas  22994  topcld  23058  ntrtop  23093  opnneissb  23137  opnssneib  23138  opnneiid  23149  maxlp  23170  isperf2  23175  restperf  23207  idcn  23280  cnconst2  23306  lmres  23323  fiuncmp  23427  1stcelcls  23484  ssref  23535  refref  23536  kgencn2  23580  ptpjpre1  23594  ptbasfi  23604  xkopt  23678  elqtop2  23724  ptcmpfi  23836  fbssfi  23860  opnfbas  23865  filtop  23878  isfil2  23879  isfild  23881  fsubbas  23890  ssfg  23895  filssufilg  23934  ufileu  23942  imaelfm  23974  rnelfm  23976  fmfnfmlem4  23980  neiflim  23997  fclscf  24048  flimfnfcls  24051  tsmsfbas  24151  xpsxmet  24405  xpsdsval  24406  xpsmet  24407  tmsxms  24514  tmsms  24515  imasf1oxms  24517  imasf1oms  24518  prdsxms  24558  prdsms  24559  tmsxpsval  24566  retopbas  24796  cnngp  24815  cnopn  24822  cnperf  24855  retopconn  24864  fsumcn  24907  abscncf  24940  recncf  24941  imcncf  24942  cjcncf  24943  mulc1cncf  24944  cncfcn1  24950  cncfmpt2f  24954  cncfmpt2ss  24955  addccncf  24956  idcncf  24957  sub1cncf  24958  sub2cncf  24959  cdivcncf  24960  negcncf  24961  negcncfOLD  24962  negfcncf  24963  abscncfALT  24964  cnmpopc  24968  xrhmeo  24990  oprpiece1res1  24995  oprpiece1res2  24996  cnrehmeo  24997  cnrehmeoOLD  24998  iscau3  25325  caubl  25355  caublcls  25356  mulcncf  25493  evthicc2  25508  ovolre  25573  volsuplem  25603  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  dyadmbllem  25647  volivth  25655  itgfsum  25876  iblabslem  25877  iblabs  25878  bddmulibl  25888  cnlimc  25937  cnlimci  25938  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  cpnord  25985  cpnres  25987  dvmptntr  26023  dvmptfsum  26027  rolle  26042  dvlipcn  26047  c1liplem1  26049  dvivth  26063  dvfsumabs  26077  ftc1a  26092  ftc1cn  26098  plyssc  26253  plyeq0  26264  0dgr  26298  coemulc  26308  coe0  26309  coesub  26310  coe1termlem  26311  dgrmulc  26325  dgrsub  26326  dvnply2  26343  plycpn  26345  plyremlem  26360  fta1lem  26363  vieta1lem2  26367  aalioulem3  26390  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmcn  26456  psercn  26484  abelth  26499  efcn  26501  efcvx  26507  dvrelog  26693  logcn  26703  dvloglem  26704  dvlog  26707  dvlog2  26709  efopnlem2  26713  logccv  26719  cxpcn  26801  cxpcnOLD  26802  cxpcn3  26805  resqrtcn  26806  sqrtcn  26807  loglesqrt  26818  atancn  26993  jensen  27046  ftalem3  27132  dchrfi  27313  dchrisumlema  27546  pntlem3  27667  madebday  27952  uhgrsubgrself  29311  uhgrspansubgr  29322  umgr2adedgwlk  29974  umgr2adedgwlkon  29975  umgr2adedgspth  29977  upgr1wlkdlem2  30174  sspid  30753  ssps  30758  helch  31271  hhssnv  31292  hhsssh  31297  shintcl  31358  chintcl  31360  shlesb1i  31414  omlsi  31432  chlejb1i  31504  chm0i  31518  chabs1  31544  chabs2  31545  spanun  31573  cmidi  31638  pjidmcoi  32205  csmdsymi  32362  sumdmdlem2  32447  dmdbr5ati  32450  mdcompli  32457  dmdcompli  32458  disjdifprg  32594  fcoinver  32623  f1rnen  32645  xppreima  32661  padct  32736  xrinfm  32764  clatp0cl  32950  clatp1cl  32951  xrsp0  32996  xrsp1  32997  cntrcrng  33055  gsumle  33083  cycpmconjslem1  33156  cycpmconjslem2  33157  gsumvsca1  33214  gsumvsca2  33215  qusxpid  33370  ellspds  33375  rspidlid  33382  rlmdim  33636  reff  33799  locfinreflem  33800  esumsnf  34044  esumcvg  34066  sigagenid  34131  iblidicc  34585  cxpcncf1  34588  fdvposlt  34592  fdvneggt  34593  fdvposle  34594  fdvnegge  34595  logdivsqrle  34643  bnj1253  35009  fineqvac  35089  cvmlift2lem6  35292  satfun  35395  mrsubrn  35497  elmrsubrn  35504  elmsubrn  35512  msubrn  35513  imagesset  35934  ivthALT  36317  fness  36331  fneref  36332  refssfne  36340  fnemeet1  36348  fnejoin2  36351  filnetlem2  36361  filnetlem4  36363  ontgval  36413  knoppcnlem10  36484  knoppcnlem11  36485  bj-rabtr  36912  bj-rabtrAUTO  36914  bj-disj2r  37010  bj-restsnid  37069  bj-resta  37078  bj-imdirco  37172  elxp8  37353  finorwe  37364  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfposadd  37653  ftc1cnnclem  37677  ftc1cnnc  37678  ftc1anc  37687  ftc2nc  37688  areacirclem2  37695  areacirclem4  37697  areacirc  37699  caures  37746  constcncf  37748  brssrid  38483  brcnvssrid  38488  refrelid  38503  n0eldmqs  38629  atpsubN  39735  pol1N  39892  dia2dimlem13  41058  dibord  41141  dochvalr  41339  hdmapevec  41817  lcmineqlem10  42019  lcmineqlem12  42021  ismrcd1  42685  ismrc  42688  incssnn0  42698  mzpclall  42714  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  aomclem6  43047  kelac1  43051  gicabl  43087  arearect  43203  areaquad  43204  unielid  43207  oege2  43296  oacl2g  43319  ofoaf  43344  clcnvlem  43612  cnvtrcl0  43615  fvilbd  43678  relexp0a  43705  corcltrcl  43728  clsk1indlem2  44031  ntrclskb  44058  wnefimgd  44150  mnuprdlem4  44270  nzss  44312  lhe4.4ex1a  44324  dvsconst  44325  dvsid  44326  dvsef  44327  binomcxplemnn0  44344  onfrALTlem3  44541  onfrALTlem3VD  44884  unisn0  44993  founiiun0  45132  evthiccabs  45448  climconstmpt  45613  cncfshift  45829  addccncf2  45831  cncfcompt  45838  ioccncflimc  45840  icocncflimc  45844  cncfiooicclem1  45848  cncfiooicc  45849  cncfiooiccre  45850  cxpcncf2  45854  add1cncf  45856  add2cncf  45857  sub1cncfd  45858  sub2cncfd  45859  dvcosre  45867  dvmptfprod  45900  ibliooicc  45926  itgsincmulx  45929  itgsubsticclem  45930  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem16  46078  fourierdlem18  46080  fourierdlem21  46083  fourierdlem22  46084  fourierdlem23  46085  fourierdlem32  46094  fourierdlem33  46095  fourierdlem39  46101  fourierdlem40  46102  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem62  46123  fourierdlem68  46129  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem83  46144  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem93  46154  fourierdlem94  46155  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  fouriercn  46187  etransclem18  46207  etransclem22  46211  etransclem34  46223  etransclem46  46235  etransclem47  46236  sge0fsum  46342  meaiininclem  46441  hoidmvlelem2  46551  hspdifhsp  46571  hspmbllem2  46582  hspmbl  46584  iinhoiicclem  46628  pimgtmnf2  46669  smflimsuplem1  46775  smflimsuplem6  46780  srhmsubcALTV  48168