Theorem ssid 3961

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 23	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
2	1	ssriv 3943	1 ⊢ 𝐴 ⊆ 𝐴

Syntax hints:   ∈ wcel 2145   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-ss 3924

This theorem is referenced by:  ssidd  3962  eqimssd  3995  eqimsscd  3996  eqimssi  3999  eqimss2i  4000  nsspssun  4223  difidALT  4333  inv1  4355  disjpss  4418  pwidgOLD  4579  elssuni  4900  unimax  4906  intmin  4929  rintn0  5071  sseliALT  5264  inxpssres  5669  xpss1  5671  xpss2  5672  residm  6000  resdm  6016  resmpt3  6031  cnvrescnv  6186  onelssex  6399  ordunidif  6400  funresfunco  6566  dffn3  6708  fdmrn  6727  fvreseq1  7024  iunpw  7758  onsucuni  7812  tfisi  7843  fparlem3  8097  fparlem4  8098  funsssuppss  8174  tfrlem1  8350  tz7.48-2  8417  oaordi  8519  omwordi  8544  omass  8553  nnaordi  8592  nnmwordi  8609  naddunif  8668  fpmg  8854  boxcutc  8927  domss2  9112  findcard2d  9139  fimax2g  9234  domunfican  9269  fipreima  9303  fimin2g  9447  wofib  9495  wemapso  9501  noinfep  9617  cantnfval2  9626  tcidm  9701  tc0  9702  r1rankidb  9764  r1pw  9805  rankr1id  9822  scott0  9848  xpomen  9987  infpwfien  10034  alephsmo  10074  dfac12lem3  10117  cflem  10216  cflemOLD  10217  cflecard  10224  cfslb  10238  fin4en1  10281  fin23lem13  10304  fin23lem36  10320  isf32lem1  10325  fin67  10367  dcomex  10419  zorn2lem4  10471  alephexp2  10554  fpwwe2lem12  10615  canthnumlem  10621  wuncidm  10719  eltsk2g  10724  axgroth6  10801  axgroth3  10804  indconst1  12222  xrsup  13892  expcl  14106  hashcard  14382  hashf1lem2  14483  xptrrel  15007  cotrtrclfv  15039  rtrclreclem2  15086  lo1eq  15609  rlimeq  15610  serclim0  15618  isercolllem2  15707  isercoll  15709  fsum2d  15812  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  fprod2d  16025  risefaccl  16059  fallfaccl  16060  eflt  16163  rpnnen2lem3  16262  rpnnen2lem5  16264  rpnnen2lem12  16271  rexpen  16274  ressbasssg  17287  ressid  17294  ressinbas  17295  oduclatb  18553  ipopos  18582  fpwipodrs  18586  qusxpid  19242  ghmghmrn  19296  elcntr  19391  cntrnsg  19405  0symgefmndeq  19455  sylow3lem5  19692  lsmss1  19726  lsmss2  19728  cmnbascntr  19866  cntrcmnd  19903  cntrabl  19904  gsumzres  19970  gsumzcl2  19971  gsumzf1o  19973  gsumadd  19984  gsumzmhm  19998  gsumzoppg  20005  dprdf1  20096  ablfac1eulem  20135  gsumle  20206  subrgid  20649  srhmsubc  20756  lbsextlem1  21251  rlmval2  21282  znf1o  21661  zntoslem  21666  css0  21799  uvcresum  21903  frlmlbs  21907  psrass1lem  22043  mdetrsca2  22722  mdetrlin2  22725  mdetunilem5  22734  mdetunilem9  22738  smadiadetglem1  22789  smadiadetglem2  22790  pmatcollpw3  22902  topopn  23024  fiinbas  23070  topbas  23090  topcld  23153  ntrtop  23188  opnneissb  23232  opnssneib  23233  opnneiid  23244  maxlp  23265  isperf2  23270  restperf  23302  idcn  23375  cnconst2  23401  lmres  23418  fiuncmp  23522  1stcelcls  23579  ssref  23630  refref  23631  kgencn2  23675  ptpjpre1  23689  ptbasfi  23699  xkopt  23773  elqtop2  23819  ptcmpfi  23931  fbssfi  23955  opnfbas  23960  filtop  23973  isfil2  23974  isfild  23976  fsubbas  23985  ssfg  23990  filssufilg  24029  ufileu  24037  imaelfm  24069  rnelfm  24071  fmfnfmlem4  24075  neiflim  24092  fclscf  24143  flimfnfcls  24146  tsmsfbas  24246  xpsxmet  24498  xpsdsval  24499  xpsmet  24500  tmsxms  24604  tmsms  24605  imasf1oxms  24607  imasf1oms  24608  prdsxms  24648  prdsms  24649  tmsxpsval  24656  retopbas  24878  cnngp  24897  cnopn  24904  cnperf  24939  retopconn  24948  fsumcn  24990  abscncf  25021  recncf  25022  imcncf  25023  cjcncf  25024  mulc1cncf  25025  cncfcn1  25031  cncfmpt2f  25035  cncfmpt2ss  25036  addccncf  25037  idcncf  25038  sub1cncf  25039  sub2cncf  25040  cdivcncf  25041  negcncf  25042  negfcncf  25043  abscncfALT  25044  cnmpopc  25048  xrhmeo  25066  oprpiece1res1  25071  oprpiece1res2  25072  cnrehmeo  25073  iscau3  25398  caubl  25428  caublcls  25429  mulcncf  25566  evthicc2  25580  ovolre  25645  volsuplem  25675  uniiccdif  25698  uniioovol  25699  uniiccvol  25700  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  dyadmbllem  25719  volivth  25727  itgfsum  25947  iblabslem  25948  iblabs  25949  bddmulibl  25959  cnlimc  26008  cnlimci  26009  dvcnp2  26040  dvcn  26041  cpnord  26055  cpnres  26057  dvmptntr  26091  dvmptfsum  26095  rolle  26110  dvlipcn  26114  c1liplem1  26116  dvivth  26130  dvfsumabs  26143  ftc1a  26157  ftc1cn  26163  plyssc  26318  plyeq0  26329  0dgr  26363  coemulc  26373  coe0  26374  coesub  26375  coe1termlem  26376  dgrmulc  26389  dgrsub  26390  dvnply2  26409  plycpn  26411  plyremlem  26426  fta1lem  26429  vieta1lem2  26433  aalioulem3  26456  taylthlem1  26494  taylthlem2  26495  ulmcn  26520  psercn  26547  abelth  26562  efcn  26564  efcvx  26570  dvrelog  26760  logcn  26770  dvloglem  26771  dvlog  26774  dvlog2  26776  efopnlem2  26780  logccv  26786  cxpcn  26868  cxpcn3  26871  resqrtcn  26872  sqrtcn  26873  loglesqrt  26884  atancn  27059  jensen  27111  ftalem3  27197  dchrfi  27377  dchrisumlema  27610  pntlem3  27731  madebday  28051  expscl  28582  bdaypw2n0bndlem  28614  uhgrsubgrself  29539  uhgrspansubgr  29550  umgr2adedgwlk  30203  umgr2adedgwlkon  30204  umgr2adedgspth  30206  upgr1wlkdlem2  30406  sspid  30986  ssps  30991  helch  31504  hhssnv  31525  hhsssh  31530  shintcl  31591  chintcl  31593  shlesb1i  31647  omlsi  31665  chlejb1i  31737  chm0i  31751  chabs1  31777  chabs2  31778  spanun  31806  cmidi  31871  pjidmcoi  32438  csmdsymi  32595  sumdmdlem2  32680  dmdbr5ati  32683  mdcompli  32690  dmdcompli  32691  disjdifprg  32830  fcoinver  32859  f1rnen  32885  xppreima  32902  padct  32975  xrinfm  33012  clatp0cl  33209  clatp1cl  33210  xrsp0  33245  xrsp1  33246  cntrcrng  33314  cycpmconjslem1  33387  cycpmconjslem2  33388  gsumvsca1  33459  gsumvsca2  33460  ellspds  33598  rspidlid  33604  rlmdim  33917  reff  34146  locfinreflem  34147  esumsnf  34371  esumcvg  34393  sigagenid  34458  iblidicc  34896  cxpcncf1  34899  fdvposlt  34903  fdvneggt  34904  fdvposle  34905  fdvnegge  34906  logdivsqrle  34954  bnj1253  35322  fineqvac  35424  fineqvnttrclse  35432  noinfepfnregs  35440  cvmlift2lem6  35671  satfun  35774  mrsubrn  35876  elmrsubrn  35883  elmsubrn  35891  msubrn  35892  imagesset  36316  ivthALT  36708  fness  36722  fneref  36723  refssfne  36731  fnemeet1  36739  fnejoin2  36742  filnetlem2  36752  filnetlem4  36754  ontgval  36804  ttctrid  36875  knoppcnlem10  36953  knoppcnlem11  36954  bj-rabtr  37427  bj-rabtrAUTO  37429  bj-disj2r  37525  bj-restsnid  37589  bj-resta  37598  bj-imdirco  37694  elxp8  37877  finorwe  37888  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  mbfposadd  38178  ftc1cnnclem  38202  ftc1cnnc  38203  ftc1anc  38212  ftc2nc  38213  areacirclem2  38220  areacirclem4  38222  areacirc  38224  caures  38271  constcncf  38273  brssrid  39093  brcnvssrid  39098  refrelid  39113  n0eldmqs  39243  atpsubN  40389  pol1N  40546  dia2dimlem13  41712  dibord  41795  dochvalr  41993  hdmapevec  42471  lcmineqlem10  42667  lcmineqlem12  42669  ismrcd1  43291  ismrc  43294  incssnn0  43304  mzpclall  43320  rmydioph  43603  rmxdioph  43605  expdiophlem2  43611  expdioph  43612  aomclem6  43648  kelac1  43652  gicabl  43688  arearect  43804  areaquad  43805  unielid  43808  oege2  43896  oacl2g  43919  ofoaf  43944  clcnvlem  44211  cnvtrcl0  44214  fvilbd  44277  relexp0a  44304  corcltrcl  44327  clsk1indlem2  44630  ntrclskb  44657  wnefimgd  44749  mnuprdlem4  44849  nzss  44891  lhe4.4ex1a  44903  dvsconst  44904  dvsid  44905  dvsef  44906  binomcxplemnn0  44923  onfrALTlem3  45118  onfrALTlem3VD  45460  unisn0  45632  founiiun0  45766  evthiccabs  46070  climconstmpt  46230  cncfshift  46446  addccncf2  46448  cncfcompt  46455  ioccncflimc  46457  icocncflimc  46461  cncfiooicclem1  46465  cncfiooicc  46466  cncfiooiccre  46467  cxpcncf2  46471  add1cncf  46473  add2cncf  46474  sub1cncfd  46475  sub2cncfd  46476  dvcosre  46484  dvmptfprod  46517  ibliooicc  46543  itgsincmulx  46546  itgsubsticclem  46547  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  dirkeritg  46674  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem16  46695  fourierdlem18  46697  fourierdlem21  46700  fourierdlem22  46701  fourierdlem23  46702  fourierdlem32  46711  fourierdlem33  46712  fourierdlem39  46718  fourierdlem40  46719  fourierdlem57  46735  fourierdlem58  46736  fourierdlem59  46737  fourierdlem62  46740  fourierdlem68  46746  fourierdlem72  46750  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem78  46756  fourierdlem83  46761  fourierdlem84  46762  fourierdlem85  46763  fourierdlem88  46766  fourierdlem93  46771  fourierdlem94  46772  fourierdlem95  46773  fourierdlem97  46775  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem112  46790  sqwvfoura  46800  sqwvfourb  46801  fouriersw  46803  fouriercn  46804  etransclem18  46824  etransclem22  46828  etransclem34  46840  etransclem46  46852  etransclem47  46853  sge0fsum  46959  meaiininclem  47058  hoidmvlelem2  47168  hspdifhsp  47188  hspmbllem2  47199  hspmbl  47201  iinhoiicclem  47245  pimgtmnf2  47286  smflimsuplem1  47392  smflimsuplem6  47397  cjnpoly  47481  srhmsubcALTV  48945  imaidfu2lem  49738  imaidfu  49739  imaidfu2  49740  setc1onsubc  50231