Theorem ssid 4005

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ssidd  4006  eqimssd  4039  eqimsscd  4040  eqimssi  4043  eqimss2i  4044  nsspssun  4258  difidALT  4372  inv1  4395  disjpss  4461  pwidg  4623  elssuni  4942  unimax  4949  intmin  4973  rintn0  5113  sseliALT  5310  inxpssres  5694  xpss1  5696  xpss2  5697  residm  6015  resdm  6027  resmpt3  6039  cnvrescnv  6195  onelssex  6413  ordunidif  6414  funresfunco  6590  dffn3  6731  fdmrn  6750  fvreseq1  7041  fimacnvOLD  7073  iunpw  7758  onsucuni  7816  tfisi  7848  fparlem3  8100  fparlem4  8101  funsssuppss  8175  tfrlem1  8376  tz7.48-2  8442  oaordi  8546  omwordi  8571  omass  8580  nnaordi  8618  nnmwordi  8635  naddunif  8692  fpmg  8862  boxcutc  8935  domss2  9136  findcard2d  9166  0fin  9171  en1eqsnOLD  9275  fimax2g  9289  domunfican  9320  pwfiOLD  9347  fipreima  9358  fimin2g  9492  wofib  9540  wemapso  9546  noinfep  9655  cantnfval2  9664  tcidm  9741  tc0  9742  r1rankidb  9799  r1pw  9840  rankr1id  9857  scott0  9881  xpomen  10010  infpwfien  10057  alephsmo  10097  dfac12lem3  10140  cflem  10241  cflecard  10248  cfslb  10261  fin4en1  10304  fin23lem13  10327  fin23lem36  10343  isf32lem1  10348  fin67  10390  dcomex  10442  zorn2lem4  10494  alephexp2  10576  fpwwe2lem12  10637  canthnumlem  10643  wuncidm  10741  eltsk2g  10746  axgroth6  10823  axgroth3  10826  xrsup  13833  expcl  14045  hashcard  14315  hashf1lem2  14417  xptrrel  14927  cotrtrclfv  14959  rtrclreclem2  15006  lo1eq  15512  rlimeq  15513  serclim0  15521  isercolllem2  15612  isercoll  15614  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  fprod2d  15925  risefaccl  15959  fallfaccl  15960  eflt  16060  rpnnen2lem3  16159  rpnnen2lem5  16161  rpnnen2lem12  16168  rexpen  16171  ressbasssg  17181  ressid  17189  ressinbas  17190  oduclatb  18460  ipopos  18489  fpwipodrs  18493  ghmghmrn  19111  elcntr  19194  cntrnsg  19208  0symgefmndeq  19261  sylow3lem5  19499  lsmss1  19533  lsmss2  19535  cmnbascntr  19673  cntrcmnd  19710  cntrabl  19711  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumadd  19791  gsumzmhm  19805  gsumzoppg  19812  dprdf1  19903  ablfac1eulem  19942  subrgid  20321  lbsextlem1  20771  rlmval2  20816  znf1o  21107  zntoslem  21112  css0  21242  uvcresum  21348  frlmlbs  21352  psrass1lemOLD  21493  psrass1lem  21496  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  mdetunilem9  22122  smadiadetglem1  22173  smadiadetglem2  22174  pmatcollpw3  22286  topopn  22408  fiinbas  22455  topbas  22475  topcld  22539  ntrtop  22574  opnneissb  22618  opnssneib  22619  opnneiid  22630  maxlp  22651  isperf2  22656  restperf  22688  idcn  22761  cnconst2  22787  lmres  22804  fiuncmp  22908  1stcelcls  22965  ssref  23016  refref  23017  kgencn2  23061  ptpjpre1  23075  ptbasfi  23085  xkopt  23159  elqtop2  23205  ptcmpfi  23317  fbssfi  23341  opnfbas  23346  filtop  23359  isfil2  23360  isfild  23362  fsubbas  23371  ssfg  23376  filssufilg  23415  ufileu  23423  imaelfm  23455  rnelfm  23457  fmfnfmlem4  23461  neiflim  23478  fclscf  23529  flimfnfcls  23532  tsmsfbas  23632  xpsxmet  23886  xpsdsval  23887  xpsmet  23888  tmsxms  23995  tmsms  23996  imasf1oxms  23998  imasf1oms  23999  prdsxms  24039  prdsms  24040  tmsxpsval  24047  retopbas  24277  cnngp  24296  cnopn  24303  cnperf  24336  retopconn  24345  fsumcn  24386  abscncf  24417  recncf  24418  imcncf  24419  cjcncf  24420  mulc1cncf  24421  cncfcn1  24427  cncfmpt2f  24431  cncfmpt2ss  24432  addccncf  24433  idcncf  24434  sub1cncf  24435  sub2cncf  24436  cdivcncf  24437  negcncf  24438  negfcncf  24439  abscncfALT  24440  cnmpopc  24444  xrhmeo  24462  oprpiece1res1  24467  oprpiece1res2  24468  cnrehmeo  24469  iscau3  24795  caubl  24825  caublcls  24826  evthicc2  24977  ovolre  25042  volsuplem  25072  uniiccdif  25095  uniioovol  25096  uniiccvol  25097  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  dyadmbllem  25116  volivth  25124  itgfsum  25344  iblabslem  25345  iblabs  25346  bddmulibl  25356  cnlimc  25405  cnlimci  25406  dvcnp2  25437  dvcn  25438  cpnord  25452  cpnres  25454  dvmptntr  25488  dvmptfsum  25492  rolle  25507  dvlipcn  25511  c1liplem1  25513  dvivth  25527  dvfsumabs  25540  ftc1a  25554  ftc1cn  25560  plyssc  25714  plyeq0  25725  0dgr  25759  coemulc  25769  coe0  25770  coesub  25771  coe1termlem  25772  dgrmulc  25785  dgrsub  25786  dvnply2  25800  plycpn  25802  plyremlem  25817  fta1lem  25820  vieta1lem2  25824  aalioulem3  25847  taylthlem1  25885  taylthlem2  25886  ulmcn  25911  psercn  25938  abelth  25953  efcn  25955  efcvx  25961  dvrelog  26145  logcn  26155  dvloglem  26156  dvlog  26159  dvlog2  26161  efopnlem2  26165  logccv  26171  cxpcn  26253  cxpcn3  26256  resqrtcn  26257  sqrtcn  26258  loglesqrt  26266  atancn  26441  jensen  26493  ftalem3  26579  dchrfi  26758  dchrisumlema  26991  pntlem3  27112  madebday  27394  uhgrsubgrself  28537  uhgrspansubgr  28548  umgr2adedgwlk  29199  umgr2adedgwlkon  29200  umgr2adedgspth  29202  upgr1wlkdlem2  29399  sspid  29978  ssps  29983  helch  30496  hhssnv  30517  hhsssh  30522  shintcl  30583  chintcl  30585  shlesb1i  30639  omlsi  30657  chlejb1i  30729  chm0i  30743  chabs1  30769  chabs2  30770  spanun  30798  cmidi  30863  pjidmcoi  31430  csmdsymi  31587  sumdmdlem2  31672  dmdbr5ati  31675  mdcompli  31682  dmdcompli  31683  disjdifprg  31806  fcoinver  31835  f1rnen  31853  xppreima  31871  padct  31944  xrinfm  31967  clatp0cl  32146  clatp1cl  32147  xrsp0  32182  xrsp1  32183  cntrcrng  32214  gsumle  32242  cycpmconjslem1  32313  cycpmconjslem2  32314  gsumvsca1  32371  gsumvsca2  32372  qusxpid  32475  ellspds  32481  rspidlid  32487  rlmdim  32694  reff  32819  locfinreflem  32820  esumsnf  33062  esumcvg  33084  sigagenid  33149  iblidicc  33604  cxpcncf1  33607  fdvposlt  33611  fdvneggt  33612  fdvposle  33613  fdvnegge  33614  logdivsqrle  33662  bnj1253  34028  fineqvac  34097  cvmlift2lem6  34299  satfun  34402  mrsubrn  34504  elmrsubrn  34511  elmsubrn  34519  msubrn  34520  imagesset  34925  gg-negcncf  35166  gg-cnrehmeo  35171  gg-mulcncf  35173  gg-dvcnp2  35174  gg-cxpcn  35184  ivthALT  35220  fness  35234  fneref  35235  refssfne  35243  fnemeet1  35251  fnejoin2  35254  filnetlem2  35264  filnetlem4  35266  ontgval  35316  knoppcnlem10  35378  knoppcnlem11  35379  bj-rabtr  35810  bj-rabtrAUTO  35812  bj-disj2r  35909  bj-restsnid  35968  bj-resta  35977  bj-imdirco  36071  elxp8  36252  finorwe  36263  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfposadd  36535  ftc1cnnclem  36559  ftc1cnnc  36560  ftc1anc  36569  ftc2nc  36570  areacirclem2  36577  areacirclem4  36579  areacirc  36581  caures  36628  constcncf  36630  brssrid  37372  brcnvssrid  37377  refrelid  37392  n0eldmqs  37518  atpsubN  38624  pol1N  38781  dia2dimlem13  39947  dibord  40030  dochvalr  40228  hdmapevec  40706  lcmineqlem10  40903  lcmineqlem12  40905  ismrcd1  41436  ismrc  41439  incssnn0  41449  mzpclall  41465  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  aomclem6  41801  kelac1  41805  gicabl  41841  arearect  41964  areaquad  41965  unielid  41968  oege2  42057  oacl2g  42080  ofoaf  42105  clcnvlem  42374  cnvtrcl0  42377  fvilbd  42440  relexp0a  42467  corcltrcl  42490  clsk1indlem2  42793  ntrclskb  42820  wnefimgd  42913  mnuprdlem4  43034  nzss  43076  lhe4.4ex1a  43088  dvsconst  43089  dvsid  43090  dvsef  43091  binomcxplemnn0  43108  onfrALTlem3  43305  onfrALTlem3VD  43648  unisn0  43741  founiiun0  43888  evthiccabs  44209  climconstmpt  44374  cncfshift  44590  addccncf2  44592  cncfcompt  44599  ioccncflimc  44601  icocncflimc  44605  cncfiooicclem1  44609  cncfiooicc  44610  cncfiooiccre  44611  cxpcncf2  44615  add1cncf  44617  add2cncf  44618  sub1cncfd  44619  sub2cncfd  44620  dvcosre  44628  dvmptfprod  44661  ibliooicc  44687  itgsincmulx  44690  itgsubsticclem  44691  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  dirkeritg  44818  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem16  44839  fourierdlem18  44841  fourierdlem21  44844  fourierdlem22  44845  fourierdlem23  44846  fourierdlem32  44855  fourierdlem33  44856  fourierdlem39  44862  fourierdlem40  44863  fourierdlem57  44879  fourierdlem58  44880  fourierdlem59  44881  fourierdlem62  44884  fourierdlem68  44890  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem83  44905  fourierdlem84  44906  fourierdlem85  44907  fourierdlem88  44910  fourierdlem93  44915  fourierdlem94  44916  fourierdlem95  44917  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  sqwvfoura  44944  sqwvfourb  44945  fouriersw  44947  fouriercn  44948  etransclem18  44968  etransclem22  44972  etransclem34  44984  etransclem46  44996  etransclem47  44997  sge0fsum  45103  meaiininclem  45202  hoidmvlelem2  45312  hspdifhsp  45332  hspmbllem2  45343  hspmbl  45345  iinhoiicclem  45389  pimgtmnf2  45430  smflimsuplem1  45536  smflimsuplem6  45541  srhmsubc  46974  srhmsubcALTV  46992