Theorem ssid 3944

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889

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

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

This theorem is referenced by:  ssidd  3945  eqimssd  3978  eqimsscd  3979  eqimssi  3982  eqimss2i  3983  nsspssun  4208  difidALT  4317  inv1  4338  disjpss  4401  pwidg  4561  elssuni  4881  unimax  4887  intmin  4910  rintn0  5051  sseliALT  5244  inxpssres  5648  xpss1  5650  xpss2  5651  residm  5975  resdm  5991  resmpt3  6003  cnvrescnv  6159  onelssex  6372  ordunidif  6373  funresfunco  6539  dffn3  6680  fdmrn  6699  fvreseq1  6991  iunpw  7725  onsucuni  7779  tfisi  7810  fparlem3  8064  fparlem4  8065  funsssuppss  8140  tfrlem1  8315  tz7.48-2  8381  oaordi  8481  omwordi  8506  omass  8515  nnaordi  8554  nnmwordi  8571  naddunif  8629  fpmg  8816  boxcutc  8889  domss2  9074  findcard2d  9101  fimax2g  9196  domunfican  9232  fipreima  9268  fimin2g  9412  wofib  9460  wemapso  9466  noinfep  9581  cantnfval2  9590  tcidm  9665  tc0  9666  r1rankidb  9728  r1pw  9769  rankr1id  9786  scott0  9810  xpomen  9937  infpwfien  9984  alephsmo  10024  dfac12lem3  10068  cflem  10167  cflemOLD  10168  cflecard  10175  cfslb  10188  fin4en1  10231  fin23lem13  10254  fin23lem36  10270  isf32lem1  10275  fin67  10317  dcomex  10369  zorn2lem4  10421  alephexp2  10504  fpwwe2lem12  10565  canthnumlem  10571  wuncidm  10669  eltsk2g  10674  axgroth6  10751  axgroth3  10754  indconst1  12172  xrsup  13827  expcl  14041  hashcard  14317  hashf1lem2  14418  xptrrel  14942  cotrtrclfv  14974  rtrclreclem2  15021  lo1eq  15530  rlimeq  15531  serclim0  15539  isercolllem2  15628  isercoll  15630  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  fprod2d  15946  risefaccl  15980  fallfaccl  15981  eflt  16084  rpnnen2lem3  16183  rpnnen2lem5  16185  rpnnen2lem12  16192  rexpen  16195  ressbasssg  17207  ressid  17214  ressinbas  17215  oduclatb  18473  ipopos  18502  fpwipodrs  18506  ghmghmrn  19210  elcntr  19305  cntrnsg  19319  0symgefmndeq  19369  sylow3lem5  19606  lsmss1  19640  lsmss2  19642  cmnbascntr  19780  cntrcmnd  19817  cntrabl  19818  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumadd  19898  gsumzmhm  19912  gsumzoppg  19919  dprdf1  20010  ablfac1eulem  20049  gsumle  20120  subrgid  20550  srhmsubc  20657  lbsextlem1  21156  rlmval2  21187  znf1o  21531  zntoslem  21536  css0  21669  uvcresum  21773  frlmlbs  21777  psrass1lem  21912  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  mdetunilem9  22585  smadiadetglem1  22636  smadiadetglem2  22637  pmatcollpw3  22749  topopn  22871  fiinbas  22917  topbas  22937  topcld  23000  ntrtop  23035  opnneissb  23079  opnssneib  23080  opnneiid  23091  maxlp  23112  isperf2  23117  restperf  23149  idcn  23222  cnconst2  23248  lmres  23265  fiuncmp  23369  1stcelcls  23426  ssref  23477  refref  23478  kgencn2  23522  ptpjpre1  23536  ptbasfi  23546  xkopt  23620  elqtop2  23666  ptcmpfi  23778  fbssfi  23802  opnfbas  23807  filtop  23820  isfil2  23821  isfild  23823  fsubbas  23832  ssfg  23837  filssufilg  23876  ufileu  23884  imaelfm  23916  rnelfm  23918  fmfnfmlem4  23922  neiflim  23939  fclscf  23990  flimfnfcls  23993  tsmsfbas  24093  xpsxmet  24345  xpsdsval  24346  xpsmet  24347  tmsxms  24451  tmsms  24452  imasf1oxms  24454  imasf1oms  24455  prdsxms  24495  prdsms  24496  tmsxpsval  24503  retopbas  24725  cnngp  24744  cnopn  24751  cnperf  24786  retopconn  24795  fsumcn  24837  abscncf  24868  recncf  24869  imcncf  24870  cjcncf  24871  mulc1cncf  24872  cncfcn1  24878  cncfmpt2f  24882  cncfmpt2ss  24883  addccncf  24884  idcncf  24885  sub1cncf  24886  sub2cncf  24887  cdivcncf  24888  negcncf  24889  negfcncf  24890  abscncfALT  24891  cnmpopc  24895  xrhmeo  24913  oprpiece1res1  24918  oprpiece1res2  24919  cnrehmeo  24920  iscau3  25245  caubl  25275  caublcls  25276  mulcncf  25413  evthicc2  25427  ovolre  25492  volsuplem  25522  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  dyadmbllem  25566  volivth  25574  itgfsum  25794  iblabslem  25795  iblabs  25796  bddmulibl  25806  cnlimc  25855  cnlimci  25856  dvcnp2  25887  dvcn  25888  cpnord  25902  cpnres  25904  dvmptntr  25938  dvmptfsum  25942  rolle  25957  dvlipcn  25961  c1liplem1  25963  dvivth  25977  dvfsumabs  25990  ftc1a  26004  ftc1cn  26010  plyssc  26165  plyeq0  26176  0dgr  26210  coemulc  26220  coe0  26221  coesub  26222  coe1termlem  26223  dgrmulc  26236  dgrsub  26237  dvnply2  26253  plycpn  26255  plyremlem  26270  fta1lem  26273  vieta1lem2  26277  aalioulem3  26300  taylthlem1  26338  taylthlem2  26339  ulmcn  26364  psercn  26391  abelth  26406  efcn  26408  efcvx  26414  dvrelog  26601  logcn  26611  dvloglem  26612  dvlog  26615  dvlog2  26617  efopnlem2  26621  logccv  26627  cxpcn  26709  cxpcn3  26712  resqrtcn  26713  sqrtcn  26714  loglesqrt  26725  atancn  26900  jensen  26952  ftalem3  27038  dchrfi  27218  dchrisumlema  27451  pntlem3  27572  madebday  27892  expscl  28423  bdaypw2n0bndlem  28455  uhgrsubgrself  29349  uhgrspansubgr  29360  umgr2adedgwlk  30013  umgr2adedgwlkon  30014  umgr2adedgspth  30016  upgr1wlkdlem2  30216  sspid  30796  ssps  30801  helch  31314  hhssnv  31335  hhsssh  31340  shintcl  31401  chintcl  31403  shlesb1i  31457  omlsi  31475  chlejb1i  31547  chm0i  31561  chabs1  31587  chabs2  31588  spanun  31616  cmidi  31681  pjidmcoi  32248  csmdsymi  32405  sumdmdlem2  32490  dmdbr5ati  32493  mdcompli  32500  dmdcompli  32501  disjdifprg  32645  fcoinver  32674  f1rnen  32701  xppreima  32718  padct  32791  xrinfm  32828  clatp0cl  33036  clatp1cl  33037  xrsp0  33072  xrsp1  33073  cntrcrng  33142  cycpmconjslem1  33215  cycpmconjslem2  33216  gsumvsca1  33287  gsumvsca2  33288  qusxpid  33423  ellspds  33428  rspidlid  33435  rlmdim  33754  reff  33983  locfinreflem  33984  esumsnf  34208  esumcvg  34230  sigagenid  34295  iblidicc  34736  cxpcncf1  34739  fdvposlt  34743  fdvneggt  34744  fdvposle  34745  fdvnegge  34746  logdivsqrle  34794  bnj1253  35159  fineqvac  35260  fineqvnttrclse  35268  noinfepfnregs  35276  cvmlift2lem6  35490  satfun  35593  mrsubrn  35695  elmrsubrn  35702  elmsubrn  35710  msubrn  35711  imagesset  36135  ivthALT  36517  fness  36531  fneref  36532  refssfne  36540  fnemeet1  36548  fnejoin2  36551  filnetlem2  36561  filnetlem4  36563  ontgval  36613  ttctrid  36684  knoppcnlem10  36762  knoppcnlem11  36763  bj-rabtr  37237  bj-rabtrAUTO  37239  bj-disj2r  37335  bj-restsnid  37399  bj-resta  37408  bj-imdirco  37504  elxp8  37687  finorwe  37698  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfposadd  37988  ftc1cnnclem  38012  ftc1cnnc  38013  ftc1anc  38022  ftc2nc  38023  areacirclem2  38030  areacirclem4  38032  areacirc  38034  caures  38081  constcncf  38083  brssrid  38903  brcnvssrid  38908  refrelid  38923  n0eldmqs  39053  atpsubN  40199  pol1N  40356  dia2dimlem13  41522  dibord  41605  dochvalr  41803  hdmapevec  42281  lcmineqlem10  42477  lcmineqlem12  42479  ismrcd1  43130  ismrc  43133  incssnn0  43143  mzpclall  43159  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  aomclem6  43487  kelac1  43491  gicabl  43527  arearect  43643  areaquad  43644  unielid  43647  oege2  43735  oacl2g  43758  ofoaf  43783  clcnvlem  44050  cnvtrcl0  44053  fvilbd  44116  relexp0a  44143  corcltrcl  44166  clsk1indlem2  44469  ntrclskb  44496  wnefimgd  44588  mnuprdlem4  44702  nzss  44744  lhe4.4ex1a  44756  dvsconst  44757  dvsid  44758  dvsef  44759  binomcxplemnn0  44776  onfrALTlem3  44971  onfrALTlem3VD  45313  unisn0  45485  founiiun0  45620  evthiccabs  45926  climconstmpt  46086  cncfshift  46302  addccncf2  46304  cncfcompt  46311  ioccncflimc  46313  icocncflimc  46317  cncfiooicclem1  46321  cncfiooicc  46322  cncfiooiccre  46323  cxpcncf2  46327  add1cncf  46329  add2cncf  46330  sub1cncfd  46331  sub2cncfd  46332  dvcosre  46340  dvmptfprod  46373  ibliooicc  46399  itgsincmulx  46402  itgsubsticclem  46403  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem16  46551  fourierdlem18  46553  fourierdlem21  46556  fourierdlem22  46557  fourierdlem23  46558  fourierdlem32  46567  fourierdlem33  46568  fourierdlem39  46574  fourierdlem40  46575  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem62  46596  fourierdlem68  46602  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem83  46617  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem93  46627  fourierdlem94  46628  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  fouriercn  46660  etransclem18  46680  etransclem22  46684  etransclem34  46696  etransclem46  46708  etransclem47  46709  sge0fsum  46815  meaiininclem  46914  hoidmvlelem2  47024  hspdifhsp  47044  hspmbllem2  47055  hspmbl  47057  iinhoiicclem  47101  pimgtmnf2  47142  smflimsuplem1  47248  smflimsuplem6  47253  cjnpoly  47337  srhmsubcALTV  48801  imaidfu2lem  49584  imaidfu  49585  imaidfu2  49586  setc1onsubc  50077