Theorem ssid 3969

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914

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 3931

This theorem is referenced by:  ssidd  3970  eqimssd  4003  eqimsscd  4004  eqimssi  4007  eqimss2i  4008  nsspssun  4231  difidALT  4340  inv1  4361  disjpss  4424  pwidg  4583  elssuni  4901  unimax  4908  intmin  4932  rintn0  5073  sseliALT  5264  inxpssres  5655  xpss1  5657  xpss2  5658  residm  5981  resdm  5997  resmpt3  6009  cnvrescnv  6168  onelssex  6381  ordunidif  6382  funresfunco  6557  dffn3  6700  fdmrn  6719  fvreseq1  7011  iunpw  7747  onsucuni  7803  tfisi  7835  fparlem3  8093  fparlem4  8094  funsssuppss  8169  tfrlem1  8344  tz7.48-2  8410  oaordi  8510  omwordi  8535  omass  8544  nnaordi  8582  nnmwordi  8599  naddunif  8657  fpmg  8841  boxcutc  8914  domss2  9100  findcard2d  9130  0finOLD  9134  en1eqsnOLD  9220  fimax2g  9233  domunfican  9272  fipreima  9309  fimin2g  9450  wofib  9498  wemapso  9504  noinfep  9613  cantnfval2  9622  tcidm  9699  tc0  9700  r1rankidb  9757  r1pw  9798  rankr1id  9815  scott0  9839  xpomen  9968  infpwfien  10015  alephsmo  10055  dfac12lem3  10099  cflem  10198  cflemOLD  10199  cflecard  10206  cfslb  10219  fin4en1  10262  fin23lem13  10285  fin23lem36  10301  isf32lem1  10306  fin67  10348  dcomex  10400  zorn2lem4  10452  alephexp2  10534  fpwwe2lem12  10595  canthnumlem  10601  wuncidm  10699  eltsk2g  10704  axgroth6  10781  axgroth3  10784  xrsup  13830  expcl  14044  hashcard  14320  hashf1lem2  14421  xptrrel  14946  cotrtrclfv  14978  rtrclreclem2  15025  lo1eq  15534  rlimeq  15535  serclim0  15543  isercolllem2  15632  isercoll  15634  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  fprod2d  15947  risefaccl  15981  fallfaccl  15982  eflt  16085  rpnnen2lem3  16184  rpnnen2lem5  16186  rpnnen2lem12  16193  rexpen  16196  ressbasssg  17207  ressid  17214  ressinbas  17215  oduclatb  18466  ipopos  18495  fpwipodrs  18499  ghmghmrn  19167  elcntr  19262  cntrnsg  19276  0symgefmndeq  19324  sylow3lem5  19561  lsmss1  19595  lsmss2  19597  cmnbascntr  19735  cntrcmnd  19772  cntrabl  19773  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumadd  19853  gsumzmhm  19867  gsumzoppg  19874  dprdf1  19965  ablfac1eulem  20004  subrgid  20482  srhmsubc  20589  lbsextlem1  21068  rlmval2  21099  znf1o  21461  zntoslem  21466  css0  21598  uvcresum  21702  frlmlbs  21706  psrass1lem  21841  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  mdetunilem9  22507  smadiadetglem1  22558  smadiadetglem2  22559  pmatcollpw3  22671  topopn  22793  fiinbas  22839  topbas  22859  topcld  22922  ntrtop  22957  opnneissb  23001  opnssneib  23002  opnneiid  23013  maxlp  23034  isperf2  23039  restperf  23071  idcn  23144  cnconst2  23170  lmres  23187  fiuncmp  23291  1stcelcls  23348  ssref  23399  refref  23400  kgencn2  23444  ptpjpre1  23458  ptbasfi  23468  xkopt  23542  elqtop2  23588  ptcmpfi  23700  fbssfi  23724  opnfbas  23729  filtop  23742  isfil2  23743  isfild  23745  fsubbas  23754  ssfg  23759  filssufilg  23798  ufileu  23806  imaelfm  23838  rnelfm  23840  fmfnfmlem4  23844  neiflim  23861  fclscf  23912  flimfnfcls  23915  tsmsfbas  24015  xpsxmet  24268  xpsdsval  24269  xpsmet  24270  tmsxms  24374  tmsms  24375  imasf1oxms  24377  imasf1oms  24378  prdsxms  24418  prdsms  24419  tmsxpsval  24426  retopbas  24648  cnngp  24667  cnopn  24674  cnperf  24709  retopconn  24718  fsumcn  24761  abscncf  24794  recncf  24795  imcncf  24796  cjcncf  24797  mulc1cncf  24798  cncfcn1  24804  cncfmpt2f  24808  cncfmpt2ss  24809  addccncf  24810  idcncf  24811  sub1cncf  24812  sub2cncf  24813  cdivcncf  24814  negcncf  24815  negcncfOLD  24816  negfcncf  24817  abscncfALT  24818  cnmpopc  24822  xrhmeo  24844  oprpiece1res1  24849  oprpiece1res2  24850  cnrehmeo  24851  cnrehmeoOLD  24852  iscau3  25178  caubl  25208  caublcls  25209  mulcncf  25346  evthicc2  25361  ovolre  25426  volsuplem  25456  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  dyadmbllem  25500  volivth  25508  itgfsum  25728  iblabslem  25729  iblabs  25730  bddmulibl  25740  cnlimc  25789  cnlimci  25790  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  cpnord  25837  cpnres  25839  dvmptntr  25875  dvmptfsum  25879  rolle  25894  dvlipcn  25899  c1liplem1  25901  dvivth  25915  dvfsumabs  25929  ftc1a  25944  ftc1cn  25950  plyssc  26105  plyeq0  26116  0dgr  26150  coemulc  26160  coe0  26161  coesub  26162  coe1termlem  26163  dgrmulc  26177  dgrsub  26178  dvnply2  26195  plycpn  26197  plyremlem  26212  fta1lem  26215  vieta1lem2  26219  aalioulem3  26242  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmcn  26308  psercn  26336  abelth  26351  efcn  26353  efcvx  26359  dvrelog  26546  logcn  26556  dvloglem  26557  dvlog  26560  dvlog2  26562  efopnlem2  26566  logccv  26572  cxpcn  26654  cxpcnOLD  26655  cxpcn3  26658  resqrtcn  26659  sqrtcn  26660  loglesqrt  26671  atancn  26846  jensen  26899  ftalem3  26985  dchrfi  27166  dchrisumlema  27399  pntlem3  27520  madebday  27811  expscl  28317  uhgrsubgrself  29207  uhgrspansubgr  29218  umgr2adedgwlk  29875  umgr2adedgwlkon  29876  umgr2adedgspth  29878  upgr1wlkdlem2  30075  sspid  30654  ssps  30659  helch  31172  hhssnv  31193  hhsssh  31198  shintcl  31259  chintcl  31261  shlesb1i  31315  omlsi  31333  chlejb1i  31405  chm0i  31419  chabs1  31445  chabs2  31446  spanun  31474  cmidi  31539  pjidmcoi  32106  csmdsymi  32263  sumdmdlem2  32348  dmdbr5ati  32351  mdcompli  32358  dmdcompli  32359  disjdifprg  32504  fcoinver  32533  f1rnen  32553  xppreima  32569  padct  32643  xrinfm  32678  clatp0cl  32902  clatp1cl  32903  xrsp0  32950  xrsp1  32951  cntrcrng  33010  gsumle  33038  cycpmconjslem1  33111  cycpmconjslem2  33112  gsumvsca1  33179  gsumvsca2  33180  qusxpid  33334  ellspds  33339  rspidlid  33346  rlmdim  33605  reff  33829  locfinreflem  33830  esumsnf  34054  esumcvg  34076  sigagenid  34141  iblidicc  34583  cxpcncf1  34586  fdvposlt  34590  fdvneggt  34591  fdvposle  34592  fdvnegge  34593  logdivsqrle  34641  bnj1253  35007  fineqvac  35087  cvmlift2lem6  35295  satfun  35398  mrsubrn  35500  elmrsubrn  35507  elmsubrn  35515  msubrn  35516  imagesset  35941  ivthALT  36323  fness  36337  fneref  36338  refssfne  36346  fnemeet1  36354  fnejoin2  36357  filnetlem2  36367  filnetlem4  36369  ontgval  36419  knoppcnlem10  36490  knoppcnlem11  36491  bj-rabtr  36918  bj-rabtrAUTO  36920  bj-disj2r  37016  bj-restsnid  37075  bj-resta  37084  bj-imdirco  37178  elxp8  37359  finorwe  37370  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfposadd  37661  ftc1cnnclem  37685  ftc1cnnc  37686  ftc1anc  37695  ftc2nc  37696  areacirclem2  37703  areacirclem4  37705  areacirc  37707  caures  37754  constcncf  37756  brssrid  38493  brcnvssrid  38498  refrelid  38513  n0eldmqs  38639  atpsubN  39747  pol1N  39904  dia2dimlem13  41070  dibord  41153  dochvalr  41351  hdmapevec  41829  lcmineqlem10  42026  lcmineqlem12  42028  ismrcd1  42686  ismrc  42689  incssnn0  42699  mzpclall  42715  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  aomclem6  43048  kelac1  43052  gicabl  43088  arearect  43204  areaquad  43205  unielid  43208  oege2  43296  oacl2g  43319  ofoaf  43344  clcnvlem  43612  cnvtrcl0  43615  fvilbd  43678  relexp0a  43705  corcltrcl  43728  clsk1indlem2  44031  ntrclskb  44058  wnefimgd  44150  mnuprdlem4  44264  nzss  44306  lhe4.4ex1a  44318  dvsconst  44319  dvsid  44320  dvsef  44321  binomcxplemnn0  44338  onfrALTlem3  44534  onfrALTlem3VD  44876  unisn0  45048  founiiun0  45184  evthiccabs  45494  climconstmpt  45656  cncfshift  45872  addccncf2  45874  cncfcompt  45881  ioccncflimc  45883  icocncflimc  45887  cncfiooicclem1  45891  cncfiooicc  45892  cncfiooiccre  45893  cxpcncf2  45897  add1cncf  45899  add2cncf  45900  sub1cncfd  45901  sub2cncfd  45902  dvcosre  45910  dvmptfprod  45943  ibliooicc  45969  itgsincmulx  45972  itgsubsticclem  45973  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem16  46121  fourierdlem18  46123  fourierdlem21  46126  fourierdlem22  46127  fourierdlem23  46128  fourierdlem32  46137  fourierdlem33  46138  fourierdlem39  46144  fourierdlem40  46145  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem62  46166  fourierdlem68  46172  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem83  46187  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem93  46197  fourierdlem94  46198  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  fouriercn  46230  etransclem18  46250  etransclem22  46254  etransclem34  46266  etransclem46  46278  etransclem47  46279  sge0fsum  46385  meaiininclem  46484  hoidmvlelem2  46594  hspdifhsp  46614  hspmbllem2  46625  hspmbl  46627  iinhoiicclem  46671  pimgtmnf2  46712  smflimsuplem1  46818  smflimsuplem6  46823  cjnpoly  46890  srhmsubcALTV  48313  imaidfu2lem  49098  imaidfu  49099  imaidfu2  49100  setc1onsubc  49591