Theorem ssid 3962

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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ss 3925

This theorem is used by:  ssidd  3963  eqimssd  3996  eqimsscd  3997  eqimssi  4000  eqimss2i  4001  nsspssun  4224  difidALT  4336  inv1  4358  disjpss  4424  disjdif  4436  pwidgOLD  4588  elssuni  4909  unimax  4915  intmin  4938  rintn0  5080  sseliALT  5277  inxpssres  5683  xpss1  5685  xpss2  5686  residm  6014  resdm  6030  resmpt3  6045  cnvrescnv  6199  onelssex  6417  ordunidif  6418  funresfunco  6584  dffn3  6725  fdmrn  6744  fvreseq1  7041  iunpw  7779  onsucuni  7833  tfisi  7864  fparlem3  8118  fparlem4  8119  funsssuppss  8195  tfrlem1  8371  tz7.48-2  8438  oaordi  8540  omwordi  8565  omass  8574  nnaordi  8613  nnmwordi  8630  naddunif  8689  fpmg  8875  boxcutc  8948  domss2  9134  findcard2d  9161  fimax2g  9256  domunfican  9291  fipreima  9325  fimin2g  9469  wofib  9517  wemapso  9523  noinfep  9639  cantnfval2  9648  tcidm  9723  tc0  9724  r1rankidb  9786  r1pw  9827  rankr1id  9844  scott0b  9876  scott0OLD  9877  xpomen  10018  infpwfien  10065  alephsmo  10105  dfac12lem3  10148  cflem  10247  cflecard  10254  cfslb  10268  fin4en1  10311  fin23lem13  10334  fin23lem36  10350  isf32lem1  10355  fin67  10397  dcomex  10449  zorn2lem4  10501  alephexp2  10584  fpwwe2lem12  10645  canthnumlem  10651  wuncidm  10749  eltsk2g  10754  axgroth6  10831  axgroth3  10834  indconst1  12249  xrsup  13921  expcl  14135  hashcard  14411  hashf1lem2  14513  xptrrel  15043  cotrtrclfv  15075  rtrclreclem2  15122  lo1eq  15645  rlimeq  15646  serclim0  15654  isercolllem2  15743  isercoll  15745  fsum2d  15848  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  fprod2d  16061  risefaccl  16095  fallfaccl  16096  eflt  16198  rpnnen2lem3  16297  rpnnen2lem5  16299  rpnnen2lem12  16306  rexpen  16309  ressbasssg  17322  ressid  17329  ressinbas  17330  oduclatb  18588  ipopos  18617  fpwipodrs  18621  qusxpid  19282  ghmghmrn  19336  elcntr  19431  cntrnsg  19445  0symgefmndeq  19495  sylow3lem5  19732  lsmss1  19766  lsmss2  19768  cmnbascntr  19906  cntrcmnd  19943  cntrabl  19944  gsumzres  20010  gsumzcl2  20011  gsumzf1o  20013  gsumadd  20024  gsumzmhm  20038  gsumzoppg  20045  dprdf1  20136  ablfac1eulem  20175  gsumle  20246  subrgid  20709  srhmsubc  20816  lbsextlem1  21319  rlmval2  21350  znf1o  21738  zntoslem  21743  css0  21876  uvcresum  21980  frlmlbs  21984  psrass1lem  22120  mdetrsca2  22798  mdetrlin2  22801  mdetunilem5  22810  mdetunilem9  22814  smadiadetglem1  22865  smadiadetglem2  22866  pmatcollpw3  22978  topopn  23100  fiinbas  23146  topbas  23166  topcld  23229  ntrtop  23264  opnneissb  23308  opnssneib  23309  opnneiid  23320  maxlp  23341  isperf2  23346  restperf  23378  idcn  23451  cnconst2  23477  lmres  23494  fiuncmp  23598  1stcelcls  23655  ssref  23706  refref  23707  kgencn2  23751  ptpjpre1  23765  ptbasfi  23775  xkopt  23849  elqtop2  23895  ptcmpfi  24007  fbssfi  24031  opnfbas  24036  filtop  24049  isfil2  24050  isfild  24052  fsubbas  24061  ssfg  24066  filssufilg  24105  ufileu  24113  imaelfm  24145  rnelfm  24147  fmfnfmlem4  24151  neiflim  24168  fclscf  24219  flimfnfcls  24222  tsmsfbas  24322  xpsxmet  24574  xpsdsval  24575  xpsmet  24576  tmsxms  24680  tmsms  24681  imasf1oxms  24683  imasf1oms  24684  prdsxms  24724  prdsms  24725  tmsxpsval  24732  retopbas  24954  cnngp  24973  cnopn  24980  cnperf  25015  retopconn  25024  fsumcn  25066  abscncf  25097  recncf  25098  imcncf  25099  cjcncf  25100  mulc1cncf  25101  cncfcn1  25107  cncfmpt2f  25111  cncfmpt2ss  25112  addccncf  25113  idcncf  25114  sub1cncf  25115  sub2cncf  25116  cdivcncf  25117  negcncf  25118  negfcncf  25119  abscncfALT  25120  cnmpopc  25124  xrhmeo  25142  oprpiece1res1  25147  oprpiece1res2  25148  cnrehmeo  25149  iscau3  25474  caubl  25504  caublcls  25505  mulcncf  25642  evthicc2  25656  ovolre  25721  volsuplem  25751  uniiccdif  25774  uniioovol  25775  uniiccvol  25776  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  dyadmbllem  25795  volivth  25803  itgfsum  26023  iblabslem  26024  iblabs  26025  bddmulibl  26035  cnlimc  26084  cnlimci  26085  dvcnp2  26116  dvcn  26117  cpnord  26131  cpnres  26133  dvmptntr  26167  dvmptfsum  26171  rolle  26186  dvlipcn  26190  c1liplem1  26192  dvivth  26206  dvfsumabs  26219  ftc1a  26233  ftc1cn  26239  plyssc  26394  plyeq0  26405  0dgr  26439  coemulc  26449  coe0  26450  coesub  26451  coe1termlem  26452  dgrmulc  26465  dgrsub  26466  dvnply2  26485  plycpn  26487  plyremlem  26502  fta1lem  26505  vieta1lem2  26509  aalioulem3  26534  taylthlem1  26573  taylthlem2  26574  ulmcn  26599  psercn  26626  abelth  26641  efcn  26643  efcvx  26649  dvrelog  26839  logcn  26849  dvloglem  26850  dvlog  26853  dvlog2  26855  efopnlem2  26859  logccv  26865  cxpcn  26947  cxpcn3  26950  resqrtcn  26951  sqrtcn  26952  loglesqrt  26963  atancn  27138  jensen  27190  ftalem3  27276  dchrfi  27456  dchrisumlema  27689  pntlem3  27810  madebday  28130  expscl  28661  bdaypw2n0bndlem  28693  uhgrsubgrself  29667  uhgrspansubgr  29678  umgr2adedgwlk  30331  umgr2adedgwlkon  30332  umgr2adedgspth  30334  upgr1wlkdlem2  30534  sspid  31114  ssps  31119  helch  31632  hhssnv  31653  hhsssh  31658  shintcl  31719  chintcl  31721  shlesb1i  31775  omlsi  31793  chlejb1i  31865  chm0i  31879  chabs1  31905  chabs2  31906  spanun  31934  cmidi  31999  pjidmcoi  32566  csmdsymi  32723  sumdmdlem2  32808  dmdbr5ati  32811  mdcompli  32818  dmdcompli  32819  disjdifprg  32957  fcoinver  32986  f1rnen  33010  xppreima  33027  padct  33100  xrinfm  33137  clatp0cl  33327  clatp1cl  33328  xrsp0  33363  xrsp1  33364  cntrcrng  33432  cycpmconjslem1  33505  cycpmconjslem2  33506  gsumvsca1  33577  gsumvsca2  33578  ellspds  33714  rspidlid  33720  rlmdim  34031  reff  34260  locfinreflem  34261  esumsnf  34485  esumcvg  34507  sigagenid  34573  iblidicc  35011  cxpcncf1  35014  fdvposlt  35018  fdvneggt  35019  fdvposle  35020  fdvnegge  35021  logdivsqrle  35069  bnj1253  35437  fineqvac  35553  fineqvnttrclse  35561  noinfepfnregs  35569  cvmlift2lem6  35821  satfun  35924  mrsubrn  36026  elmrsubrn  36033  elmsubrn  36041  msubrn  36042  imagesset  36466  nmuladdss  36726  ivthALT  36887  fness  36901  fneref  36902  refssfne  36910  fnemeet1  36918  fnejoin2  36921  filnetlem2  36931  filnetlem4  36933  ontgval  36983  ttctrid  37054  knoppcnlem10  37132  knoppcnlem11  37133  bj-rabtr  37607  bj-rabtrAUTO  37609  bj-disj2r  37705  bj-restsnid  37770  bj-resta  37779  bj-imdirco  37875  elxp8  38058  finorwe  38069  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  mbfposadd  38359  ftc1cnnclem  38383  ftc1cnnc  38384  ftc1anc  38393  ftc2nc  38394  areacirclem2  38401  areacirclem4  38403  areacirc  38405  caures  38452  constcncf  38454  brssrid  39272  brcnvssrid  39277  refrelid  39292  n0eldmqs  39422  atpsubN  40568  pol1N  40725  dia2dimlem13  41891  dibord  41974  dochvalr  42172  hdmapevec  42650  lcmineqlem10  42846  lcmineqlem12  42848  ismrcd1  43470  ismrc  43473  incssnn0  43483  mzpclall  43499  rmydioph  43782  rmxdioph  43784  expdiophlem2  43790  expdioph  43791  aomclem6  43827  kelac1  43831  gicabl  43867  arearect  43983  areaquad  43984  unielid  43987  oege2  44075  oacl2g  44098  ofoaf  44123  clcnvlem  44390  cnvtrcl0  44393  fvilbd  44456  relexp0a  44483  corcltrcl  44506  clsk1indlem2  44809  ntrclskb  44836  wnefimgd  44928  mnuprdlem4  45026  nzss  45068  lhe4.4ex1a  45080  dvsconst  45081  dvsid  45082  dvsef  45083  binomcxplemnn0  45100  onfrALTlem3  45294  onfrALTlem3VD  45636  unisn0  45815  founiiun0  45949  evthiccabs  46253  climconstmpt  46413  cncfshift  46629  addccncf2  46631  cncfcompt  46638  ioccncflimc  46640  icocncflimc  46644  cncfiooicclem1  46648  cncfiooicc  46649  cncfiooiccre  46650  cxpcncf2  46654  add1cncf  46656  add2cncf  46657  sub1cncfd  46658  sub2cncfd  46659  dvcosre  46667  dvmptfprod  46700  ibliooicc  46726  itgsincmulx  46729  itgsubsticclem  46730  itgiccshift  46735  itgperiod  46736  itgsbtaddcnst  46737  dirkeritg  46857  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem16  46878  fourierdlem18  46880  fourierdlem21  46883  fourierdlem22  46884  fourierdlem23  46885  fourierdlem32  46894  fourierdlem33  46895  fourierdlem39  46901  fourierdlem40  46902  fourierdlem57  46918  fourierdlem58  46919  fourierdlem59  46920  fourierdlem62  46923  fourierdlem68  46929  fourierdlem72  46933  fourierdlem73  46934  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem78  46939  fourierdlem83  46944  fourierdlem84  46945  fourierdlem85  46946  fourierdlem88  46949  fourierdlem93  46954  fourierdlem94  46955  fourierdlem95  46956  fourierdlem97  46958  fourierdlem101  46962  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fourierdlem112  46973  sqwvfoura  46983  sqwvfourb  46984  fouriersw  46986  fouriercn  46987  etransclem18  47007  etransclem22  47011  etransclem34  47023  etransclem46  47035  etransclem47  47036  sge0fsum  47142  meaiininclem  47241  hoidmvlelem2  47351  hspdifhsp  47371  hspmbllem2  47382  hspmbl  47384  iinhoiicclem  47428  pimgtmnf2  47469  smflimsuplem1  47575  smflimsuplem6  47580  cjnpoly  47667  srhmsubcALTV  49131  imaidfu2lem  49928  imaidfu  49929  imaidfu2  49930  setc1onsubc  50421