Theorem ssid 3945

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890

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 3907

This theorem is referenced by:  ssidd  3946  eqimssd  3979  eqimsscd  3980  eqimssi  3983  eqimss2i  3984  nsspssun  4209  difidALT  4318  inv1  4339  disjpss  4402  pwidg  4562  elssuni  4882  unimax  4888  intmin  4911  rintn0  5052  sseliALT  5244  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  6985  iunpw  7718  onsucuni  7772  tfisi  7803  fparlem3  8057  fparlem4  8058  funsssuppss  8133  tfrlem1  8308  tz7.48-2  8374  oaordi  8474  omwordi  8499  omass  8508  nnaordi  8547  nnmwordi  8564  naddunif  8622  fpmg  8809  boxcutc  8882  domss2  9067  findcard2d  9094  fimax2g  9189  domunfican  9225  fipreima  9261  fimin2g  9405  wofib  9453  wemapso  9459  noinfep  9572  cantnfval2  9581  tcidm  9656  tc0  9657  r1rankidb  9719  r1pw  9760  rankr1id  9777  scott0  9801  xpomen  9928  infpwfien  9975  alephsmo  10015  dfac12lem3  10059  cflem  10158  cflemOLD  10159  cflecard  10166  cfslb  10179  fin4en1  10222  fin23lem13  10245  fin23lem36  10261  isf32lem1  10266  fin67  10308  dcomex  10360  zorn2lem4  10412  alephexp2  10495  fpwwe2lem12  10556  canthnumlem  10562  wuncidm  10660  eltsk2g  10665  axgroth6  10742  axgroth3  10745  indconst1  12163  xrsup  13818  expcl  14032  hashcard  14308  hashf1lem2  14409  xptrrel  14933  cotrtrclfv  14965  rtrclreclem2  15012  lo1eq  15521  rlimeq  15522  serclim0  15530  isercolllem2  15619  isercoll  15621  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  fprod2d  15937  risefaccl  15971  fallfaccl  15972  eflt  16075  rpnnen2lem3  16174  rpnnen2lem5  16176  rpnnen2lem12  16183  rexpen  16186  ressbasssg  17198  ressid  17205  ressinbas  17206  oduclatb  18464  ipopos  18493  fpwipodrs  18497  ghmghmrn  19201  elcntr  19296  cntrnsg  19310  0symgefmndeq  19360  sylow3lem5  19597  lsmss1  19631  lsmss2  19633  cmnbascntr  19771  cntrcmnd  19808  cntrabl  19809  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumadd  19889  gsumzmhm  19903  gsumzoppg  19910  dprdf1  20001  ablfac1eulem  20040  gsumle  20111  subrgid  20541  srhmsubc  20648  lbsextlem1  21148  rlmval2  21179  znf1o  21541  zntoslem  21546  css0  21679  uvcresum  21783  frlmlbs  21787  psrass1lem  21922  mdetrsca2  22579  mdetrlin2  22582  mdetunilem5  22591  mdetunilem9  22595  smadiadetglem1  22646  smadiadetglem2  22647  pmatcollpw3  22759  topopn  22881  fiinbas  22927  topbas  22947  topcld  23010  ntrtop  23045  opnneissb  23089  opnssneib  23090  opnneiid  23101  maxlp  23122  isperf2  23127  restperf  23159  idcn  23232  cnconst2  23258  lmres  23275  fiuncmp  23379  1stcelcls  23436  ssref  23487  refref  23488  kgencn2  23532  ptpjpre1  23546  ptbasfi  23556  xkopt  23630  elqtop2  23676  ptcmpfi  23788  fbssfi  23812  opnfbas  23817  filtop  23830  isfil2  23831  isfild  23833  fsubbas  23842  ssfg  23847  filssufilg  23886  ufileu  23894  imaelfm  23926  rnelfm  23928  fmfnfmlem4  23932  neiflim  23949  fclscf  24000  flimfnfcls  24003  tsmsfbas  24103  xpsxmet  24355  xpsdsval  24356  xpsmet  24357  tmsxms  24461  tmsms  24462  imasf1oxms  24464  imasf1oms  24465  prdsxms  24505  prdsms  24506  tmsxpsval  24513  retopbas  24735  cnngp  24754  cnopn  24761  cnperf  24796  retopconn  24805  fsumcn  24847  abscncf  24878  recncf  24879  imcncf  24880  cjcncf  24881  mulc1cncf  24882  cncfcn1  24888  cncfmpt2f  24892  cncfmpt2ss  24893  addccncf  24894  idcncf  24895  sub1cncf  24896  sub2cncf  24897  cdivcncf  24898  negcncf  24899  negfcncf  24900  abscncfALT  24901  cnmpopc  24905  xrhmeo  24923  oprpiece1res1  24928  oprpiece1res2  24929  cnrehmeo  24930  iscau3  25255  caubl  25285  caublcls  25286  mulcncf  25423  evthicc2  25437  ovolre  25502  volsuplem  25532  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  dyadmbllem  25576  volivth  25584  itgfsum  25804  iblabslem  25805  iblabs  25806  bddmulibl  25816  cnlimc  25865  cnlimci  25866  dvcnp2  25897  dvcn  25898  cpnord  25912  cpnres  25914  dvmptntr  25948  dvmptfsum  25952  rolle  25967  dvlipcn  25971  c1liplem1  25973  dvivth  25987  dvfsumabs  26000  ftc1a  26014  ftc1cn  26020  plyssc  26175  plyeq0  26186  0dgr  26220  coemulc  26230  coe0  26231  coesub  26232  coe1termlem  26233  dgrmulc  26246  dgrsub  26247  dvnply2  26264  plycpn  26266  plyremlem  26281  fta1lem  26284  vieta1lem2  26288  aalioulem3  26311  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmcn  26377  psercn  26404  abelth  26419  efcn  26421  efcvx  26427  dvrelog  26614  logcn  26624  dvloglem  26625  dvlog  26628  dvlog2  26630  efopnlem2  26634  logccv  26640  cxpcn  26722  cxpcn3  26725  resqrtcn  26726  sqrtcn  26727  loglesqrt  26738  atancn  26913  jensen  26966  ftalem3  27052  dchrfi  27232  dchrisumlema  27465  pntlem3  27586  madebday  27906  expscl  28437  bdaypw2n0bndlem  28469  uhgrsubgrself  29363  uhgrspansubgr  29374  umgr2adedgwlk  30028  umgr2adedgwlkon  30029  umgr2adedgspth  30031  upgr1wlkdlem2  30231  sspid  30811  ssps  30816  helch  31329  hhssnv  31350  hhsssh  31355  shintcl  31416  chintcl  31418  shlesb1i  31472  omlsi  31490  chlejb1i  31562  chm0i  31576  chabs1  31602  chabs2  31603  spanun  31631  cmidi  31696  pjidmcoi  32263  csmdsymi  32420  sumdmdlem2  32505  dmdbr5ati  32508  mdcompli  32515  dmdcompli  32516  disjdifprg  32660  fcoinver  32689  f1rnen  32716  xppreima  32733  padct  32806  xrinfm  32843  clatp0cl  33051  clatp1cl  33052  xrsp0  33087  xrsp1  33088  cntrcrng  33157  cycpmconjslem1  33230  cycpmconjslem2  33231  gsumvsca1  33302  gsumvsca2  33303  qusxpid  33438  ellspds  33443  rspidlid  33450  rlmdim  33769  reff  33999  locfinreflem  34000  esumsnf  34224  esumcvg  34246  sigagenid  34311  iblidicc  34752  cxpcncf1  34755  fdvposlt  34759  fdvneggt  34760  fdvposle  34761  fdvnegge  34762  logdivsqrle  34810  bnj1253  35175  fineqvac  35276  fineqvnttrclse  35284  noinfepfnregs  35292  cvmlift2lem6  35506  satfun  35609  mrsubrn  35711  elmrsubrn  35718  elmsubrn  35726  msubrn  35727  imagesset  36151  ivthALT  36533  fness  36547  fneref  36548  refssfne  36556  fnemeet1  36564  fnejoin2  36567  filnetlem2  36577  filnetlem4  36579  ontgval  36629  ttctrid  36700  knoppcnlem10  36778  knoppcnlem11  36779  bj-rabtr  37253  bj-rabtrAUTO  37255  bj-disj2r  37351  bj-restsnid  37415  bj-resta  37424  bj-imdirco  37520  elxp8  37701  finorwe  37712  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  mbfposadd  38002  ftc1cnnclem  38026  ftc1cnnc  38027  ftc1anc  38036  ftc2nc  38037  areacirclem2  38044  areacirclem4  38046  areacirc  38048  caures  38095  constcncf  38097  brssrid  38917  brcnvssrid  38922  refrelid  38937  n0eldmqs  39067  atpsubN  40213  pol1N  40370  dia2dimlem13  41536  dibord  41619  dochvalr  41817  hdmapevec  42295  lcmineqlem10  42491  lcmineqlem12  42493  ismrcd1  43144  ismrc  43147  incssnn0  43157  mzpclall  43173  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  aomclem6  43505  kelac1  43509  gicabl  43545  arearect  43661  areaquad  43662  unielid  43665  oege2  43753  oacl2g  43776  ofoaf  43801  clcnvlem  44068  cnvtrcl0  44071  fvilbd  44134  relexp0a  44161  corcltrcl  44184  clsk1indlem2  44487  ntrclskb  44514  wnefimgd  44606  mnuprdlem4  44720  nzss  44762  lhe4.4ex1a  44774  dvsconst  44775  dvsid  44776  dvsef  44777  binomcxplemnn0  44794  onfrALTlem3  44989  onfrALTlem3VD  45331  unisn0  45503  founiiun0  45638  evthiccabs  45944  climconstmpt  46104  cncfshift  46320  addccncf2  46322  cncfcompt  46329  ioccncflimc  46331  icocncflimc  46335  cncfiooicclem1  46339  cncfiooicc  46340  cncfiooiccre  46341  cxpcncf2  46345  add1cncf  46347  add2cncf  46348  sub1cncfd  46349  sub2cncfd  46350  dvcosre  46358  dvmptfprod  46391  ibliooicc  46417  itgsincmulx  46420  itgsubsticclem  46421  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  dirkeritg  46548  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem16  46569  fourierdlem18  46571  fourierdlem21  46574  fourierdlem22  46575  fourierdlem23  46576  fourierdlem32  46585  fourierdlem33  46586  fourierdlem39  46592  fourierdlem40  46593  fourierdlem57  46609  fourierdlem58  46610  fourierdlem59  46611  fourierdlem62  46614  fourierdlem68  46620  fourierdlem72  46624  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem83  46635  fourierdlem84  46636  fourierdlem85  46637  fourierdlem88  46640  fourierdlem93  46645  fourierdlem94  46646  fourierdlem95  46647  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  fouriercn  46678  etransclem18  46698  etransclem22  46702  etransclem34  46714  etransclem46  46726  etransclem47  46727  sge0fsum  46833  meaiininclem  46932  hoidmvlelem2  47042  hspdifhsp  47062  hspmbllem2  47073  hspmbl  47075  iinhoiicclem  47119  pimgtmnf2  47160  smflimsuplem1  47266  smflimsuplem6  47271  cjnpoly  47349  srhmsubcALTV  48813  imaidfu2lem  49596  imaidfu  49597  imaidfu2  49598  setc1onsubc  50089