Theorem ssid 4001

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

Syntax hints:   ∈ wcel 2099   ⊆ wss 3946

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

This theorem depends on definitions:  df-bi 206  df-ss 3963

This theorem is referenced by:  ssidd  4002  eqimssd  4035  eqimsscd  4036  eqimssi  4039  eqimss2i  4040  nsspssun  4256  difidALT  4369  inv1  4392  disjpss  4455  pwidg  4617  elssuni  4937  unimax  4944  intmin  4968  rintn0  5109  sseliALT  5306  inxpssres  5691  xpss1  5693  xpss2  5694  residm  6011  resdm  6027  resmpt3  6039  cnvrescnv  6198  onelssex  6416  ordunidif  6417  funresfunco  6592  dffn3  6732  fdmrn  6752  fvreseq1  7044  fimacnvOLD  7076  iunpw  7771  onsucuni  7829  tfisi  7861  fparlem3  8120  fparlem4  8121  funsssuppss  8196  tfrlem1  8398  tz7.48-2  8464  oaordi  8568  omwordi  8593  omass  8602  nnaordi  8640  nnmwordi  8657  naddunif  8715  fpmg  8889  boxcutc  8962  domss2  9166  findcard2d  9196  0finOLD  9201  en1eqsnOLD  9302  fimax2g  9316  domunfican  9356  pwfiOLD  9384  fipreima  9395  fimin2g  9533  wofib  9581  wemapso  9587  noinfep  9696  cantnfval2  9705  tcidm  9782  tc0  9783  r1rankidb  9840  r1pw  9881  rankr1id  9898  scott0  9922  xpomen  10051  infpwfien  10098  alephsmo  10138  dfac12lem3  10181  cflem  10280  cflecard  10287  cfslb  10300  fin4en1  10343  fin23lem13  10366  fin23lem36  10382  isf32lem1  10387  fin67  10429  dcomex  10481  zorn2lem4  10533  alephexp2  10615  fpwwe2lem12  10676  canthnumlem  10682  wuncidm  10780  eltsk2g  10785  axgroth6  10862  axgroth3  10865  xrsup  13882  expcl  14093  hashcard  14367  hashf1lem2  14470  xptrrel  14980  cotrtrclfv  15012  rtrclreclem2  15059  lo1eq  15565  rlimeq  15566  serclim0  15574  isercolllem2  15665  isercoll  15667  fsum2d  15770  fsumabs  15800  fsumrlim  15810  fsumo1  15811  fsumiun  15820  fprod2d  15978  risefaccl  16012  fallfaccl  16013  eflt  16114  rpnnen2lem3  16213  rpnnen2lem5  16215  rpnnen2lem12  16222  rexpen  16225  ressbasssg  17245  ressid  17253  ressinbas  17254  oduclatb  18527  ipopos  18556  fpwipodrs  18560  ghmghmrn  19225  elcntr  19320  cntrnsg  19334  0symgefmndeq  19387  sylow3lem5  19625  lsmss1  19659  lsmss2  19661  cmnbascntr  19799  cntrcmnd  19836  cntrabl  19837  gsumzres  19903  gsumzcl2  19904  gsumzf1o  19906  gsumadd  19917  gsumzmhm  19931  gsumzoppg  19938  dprdf1  20029  ablfac1eulem  20068  subrgid  20553  srhmsubc  20654  lbsextlem1  21135  rlmval2  21174  znf1o  21545  zntoslem  21550  css0  21681  uvcresum  21787  frlmlbs  21791  psrass1lemOLD  21934  psrass1lem  21937  mdetrsca2  22594  mdetrlin2  22597  mdetunilem5  22606  mdetunilem9  22610  smadiadetglem1  22661  smadiadetglem2  22662  pmatcollpw3  22774  topopn  22896  fiinbas  22943  topbas  22963  topcld  23027  ntrtop  23062  opnneissb  23106  opnssneib  23107  opnneiid  23118  maxlp  23139  isperf2  23144  restperf  23176  idcn  23249  cnconst2  23275  lmres  23292  fiuncmp  23396  1stcelcls  23453  ssref  23504  refref  23505  kgencn2  23549  ptpjpre1  23563  ptbasfi  23573  xkopt  23647  elqtop2  23693  ptcmpfi  23805  fbssfi  23829  opnfbas  23834  filtop  23847  isfil2  23848  isfild  23850  fsubbas  23859  ssfg  23864  filssufilg  23903  ufileu  23911  imaelfm  23943  rnelfm  23945  fmfnfmlem4  23949  neiflim  23966  fclscf  24017  flimfnfcls  24020  tsmsfbas  24120  xpsxmet  24374  xpsdsval  24375  xpsmet  24376  tmsxms  24483  tmsms  24484  imasf1oxms  24486  imasf1oms  24487  prdsxms  24527  prdsms  24528  tmsxpsval  24535  retopbas  24765  cnngp  24784  cnopn  24791  cnperf  24824  retopconn  24833  fsumcn  24876  abscncf  24909  recncf  24910  imcncf  24911  cjcncf  24912  mulc1cncf  24913  cncfcn1  24919  cncfmpt2f  24923  cncfmpt2ss  24924  addccncf  24925  idcncf  24926  sub1cncf  24927  sub2cncf  24928  cdivcncf  24929  negcncf  24930  negcncfOLD  24931  negfcncf  24932  abscncfALT  24933  cnmpopc  24937  xrhmeo  24959  oprpiece1res1  24964  oprpiece1res2  24965  cnrehmeo  24966  cnrehmeoOLD  24967  iscau3  25294  caubl  25324  caublcls  25325  mulcncf  25462  evthicc2  25477  ovolre  25542  volsuplem  25572  uniiccdif  25595  uniioovol  25596  uniiccvol  25597  uniioombllem3  25602  uniioombllem4  25603  uniioombllem5  25604  dyadmbllem  25616  volivth  25624  itgfsum  25844  iblabslem  25845  iblabs  25846  bddmulibl  25856  cnlimc  25905  cnlimci  25906  dvcnp2  25937  dvcnp2OLD  25938  dvcn  25939  cpnord  25953  cpnres  25955  dvmptntr  25991  dvmptfsum  25995  rolle  26010  dvlipcn  26015  c1liplem1  26017  dvivth  26031  dvfsumabs  26045  ftc1a  26060  ftc1cn  26066  plyssc  26224  plyeq0  26235  0dgr  26269  coemulc  26279  coe0  26280  coesub  26281  coe1termlem  26282  dgrmulc  26296  dgrsub  26297  dvnply2  26312  plycpn  26314  plyremlem  26329  fta1lem  26332  vieta1lem2  26336  aalioulem3  26359  taylthlem1  26398  taylthlem2  26399  taylthlem2OLD  26400  ulmcn  26425  psercn  26453  abelth  26468  efcn  26470  efcvx  26476  dvrelog  26661  logcn  26671  dvloglem  26672  dvlog  26675  dvlog2  26677  efopnlem2  26681  logccv  26687  cxpcn  26769  cxpcnOLD  26770  cxpcn3  26773  resqrtcn  26774  sqrtcn  26775  loglesqrt  26786  atancn  26961  jensen  27014  ftalem3  27100  dchrfi  27281  dchrisumlema  27514  pntlem3  27635  madebday  27920  uhgrsubgrself  29213  uhgrspansubgr  29224  umgr2adedgwlk  29876  umgr2adedgwlkon  29877  umgr2adedgspth  29879  upgr1wlkdlem2  30076  sspid  30655  ssps  30660  helch  31173  hhssnv  31194  hhsssh  31199  shintcl  31260  chintcl  31262  shlesb1i  31316  omlsi  31334  chlejb1i  31406  chm0i  31420  chabs1  31446  chabs2  31447  spanun  31475  cmidi  31540  pjidmcoi  32107  csmdsymi  32264  sumdmdlem2  32349  dmdbr5ati  32352  mdcompli  32359  dmdcompli  32360  disjdifprg  32495  fcoinver  32524  f1rnen  32546  xppreima  32563  padct  32633  xrinfm  32661  clatp0cl  32849  clatp1cl  32850  xrsp0  32895  xrsp1  32896  cntrcrng  32935  gsumle  32963  cycpmconjslem1  33036  cycpmconjslem2  33037  gsumvsca1  33094  gsumvsca2  33095  qusxpid  33244  ellspds  33249  rspidlid  33256  rlmdim  33510  reff  33667  locfinreflem  33668  esumsnf  33910  esumcvg  33932  sigagenid  33997  iblidicc  34451  cxpcncf1  34454  fdvposlt  34458  fdvneggt  34459  fdvposle  34460  fdvnegge  34461  logdivsqrle  34509  bnj1253  34875  fineqvac  34946  cvmlift2lem6  35149  satfun  35252  mrsubrn  35354  elmrsubrn  35361  elmsubrn  35369  msubrn  35370  imagesset  35790  ivthALT  36060  fness  36074  fneref  36075  refssfne  36083  fnemeet1  36091  fnejoin2  36094  filnetlem2  36104  filnetlem4  36106  ontgval  36156  knoppcnlem10  36218  knoppcnlem11  36219  bj-rabtr  36649  bj-rabtrAUTO  36651  bj-disj2r  36748  bj-restsnid  36807  bj-resta  36816  bj-imdirco  36910  elxp8  37091  finorwe  37102  mblfinlem3  37373  mblfinlem4  37374  ismblfin  37375  ovoliunnfl  37376  voliunnfl  37378  volsupnfl  37379  mbfposadd  37381  ftc1cnnclem  37405  ftc1cnnc  37406  ftc1anc  37415  ftc2nc  37416  areacirclem2  37423  areacirclem4  37425  areacirc  37427  caures  37474  constcncf  37476  brssrid  38213  brcnvssrid  38218  refrelid  38233  n0eldmqs  38359  atpsubN  39465  pol1N  39622  dia2dimlem13  40788  dibord  40871  dochvalr  41069  hdmapevec  41547  lcmineqlem10  41750  lcmineqlem12  41752  ismrcd1  42392  ismrc  42395  incssnn0  42405  mzpclall  42421  rmydioph  42709  rmxdioph  42711  expdiophlem2  42717  expdioph  42718  aomclem6  42757  kelac1  42761  gicabl  42797  arearect  42917  areaquad  42918  unielid  42921  oege2  43010  oacl2g  43033  ofoaf  43058  clcnvlem  43327  cnvtrcl0  43330  fvilbd  43393  relexp0a  43420  corcltrcl  43443  clsk1indlem2  43746  ntrclskb  43773  wnefimgd  43865  mnuprdlem4  43986  nzss  44028  lhe4.4ex1a  44040  dvsconst  44041  dvsid  44042  dvsef  44043  binomcxplemnn0  44060  onfrALTlem3  44257  onfrALTlem3VD  44600  unisn0  44692  founiiun0  44833  evthiccabs  45150  climconstmpt  45315  cncfshift  45531  addccncf2  45533  cncfcompt  45540  ioccncflimc  45542  icocncflimc  45546  cncfiooicclem1  45550  cncfiooicc  45551  cncfiooiccre  45552  cxpcncf2  45556  add1cncf  45558  add2cncf  45559  sub1cncfd  45560  sub2cncfd  45561  dvcosre  45569  dvmptfprod  45602  ibliooicc  45628  itgsincmulx  45631  itgsubsticclem  45632  itgiccshift  45637  itgperiod  45638  itgsbtaddcnst  45639  dirkeritg  45759  dirkercncflem2  45761  dirkercncflem4  45763  fourierdlem16  45780  fourierdlem18  45782  fourierdlem21  45785  fourierdlem22  45786  fourierdlem23  45787  fourierdlem32  45796  fourierdlem33  45797  fourierdlem39  45803  fourierdlem40  45804  fourierdlem57  45820  fourierdlem58  45821  fourierdlem59  45822  fourierdlem62  45825  fourierdlem68  45831  fourierdlem72  45835  fourierdlem73  45836  fourierdlem74  45837  fourierdlem75  45838  fourierdlem76  45839  fourierdlem78  45841  fourierdlem83  45846  fourierdlem84  45847  fourierdlem85  45848  fourierdlem88  45851  fourierdlem93  45856  fourierdlem94  45857  fourierdlem95  45858  fourierdlem97  45860  fourierdlem101  45864  fourierdlem103  45866  fourierdlem104  45867  fourierdlem111  45874  fourierdlem112  45875  fourierdlem113  45876  sqwvfoura  45885  sqwvfourb  45886  fouriersw  45888  fouriercn  45889  etransclem18  45909  etransclem22  45913  etransclem34  45925  etransclem46  45937  etransclem47  45938  sge0fsum  46044  meaiininclem  46143  hoidmvlelem2  46253  hspdifhsp  46273  hspmbllem2  46284  hspmbl  46286  iinhoiicclem  46330  pimgtmnf2  46371  smflimsuplem1  46477  smflimsuplem6  46482  srhmsubcALTV  47738