Theorem ssid 3939

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssidd  3940  eqimssi  3975  eqimss2i  3976  nsspssun  4188  difidALT  4302  inv1  4325  disjpss  4391  pwidg  4552  elssuni  4868  unimax  4874  intmin  4896  rintn0  5034  sseliALT  5228  inxpssres  5597  xpss1  5599  xpss2  5600  residm  5913  resdm  5925  resmpt3  5935  cnvrescnv  6087  ordunidif  6299  funresfunco  6459  dffn3  6597  fdmrn  6616  fvreseq1  6898  fimacnvOLD  6930  iunpw  7599  onsucuni  7650  tfisi  7680  fparlem3  7925  fparlem4  7926  funsssuppss  7977  tfrlem1  8178  tz7.48-2  8243  oaordi  8339  omwordi  8364  omass  8373  nnaordi  8411  nnmwordi  8428  fpmg  8614  boxcutc  8687  domss2  8872  findcard2d  8911  0fin  8916  en1eqsn  8977  fimax2g  8990  domunfican  9017  pwfiOLD  9044  fipreima  9055  fimin2g  9186  wofib  9234  wemapso  9240  noinfep  9348  cantnfval2  9357  trpredtr  9408  tcidm  9435  tc0  9436  r1rankidb  9493  r1pw  9534  rankr1id  9551  scott0  9575  xpomen  9702  infpwfien  9749  alephsmo  9789  dfac12lem3  9832  cflem  9933  cflecard  9940  cfslb  9953  fin4en1  9996  fin23lem13  10019  fin23lem36  10035  isf32lem1  10040  fin67  10082  dcomex  10134  zorn2lem4  10186  alephexp2  10268  fpwwe2lem12  10329  canthnumlem  10335  wuncidm  10433  eltsk2g  10438  axgroth6  10515  axgroth3  10518  xrsup  13516  expcl  13728  hashcard  13998  hashf1lem2  14098  xptrrel  14619  cotrtrclfv  14651  rtrclreclem2  14698  lo1eq  15205  rlimeq  15206  serclim0  15214  isercolllem2  15305  isercoll  15307  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  fprod2d  15619  risefaccl  15653  fallfaccl  15654  eflt  15754  rpnnen2lem3  15853  rpnnen2lem5  15855  rpnnen2lem12  15862  rexpen  15865  ressid  16880  ressinbas  16881  oduclatb  18140  ipopos  18169  fpwipodrs  18173  ghmghmrn  18768  cntrnsg  18863  0symgefmndeq  18916  sylow3lem5  19151  lsmss1  19186  lsmss2  19188  cntrcmnd  19358  cntrabl  19359  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumadd  19439  gsumzmhm  19453  gsumzoppg  19460  dprdf1  19551  ablfac1eulem  19590  subrgid  19941  lbsextlem1  20335  rlmval2  20377  znf1o  20671  zntoslem  20676  css0  20806  uvcresum  20910  frlmlbs  20914  psrass1lemOLD  21053  psrass1lem  21056  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  mdetunilem9  21677  smadiadetglem1  21728  smadiadetglem2  21729  pmatcollpw3  21841  topopn  21963  fiinbas  22010  topbas  22030  topcld  22094  ntrtop  22129  opnneissb  22173  opnssneib  22174  opnneiid  22185  maxlp  22206  isperf2  22211  restperf  22243  idcn  22316  cnconst2  22342  lmres  22359  fiuncmp  22463  1stcelcls  22520  ssref  22571  refref  22572  kgencn2  22616  ptpjpre1  22630  ptbasfi  22640  xkopt  22714  elqtop2  22760  ptcmpfi  22872  fbssfi  22896  opnfbas  22901  filtop  22914  isfil2  22915  isfild  22917  fsubbas  22926  ssfg  22931  filssufilg  22970  ufileu  22978  imaelfm  23010  rnelfm  23012  fmfnfmlem4  23016  neiflim  23033  fclscf  23084  flimfnfcls  23087  tsmsfbas  23187  xpsxmet  23441  xpsdsval  23442  xpsmet  23443  tmsxms  23548  tmsms  23549  imasf1oxms  23551  imasf1oms  23552  prdsxms  23592  prdsms  23593  tmsxpsval  23600  retopbas  23830  cnngp  23849  cnopn  23856  cnperf  23889  retopconn  23898  fsumcn  23939  abscncf  23970  recncf  23971  imcncf  23972  cjcncf  23973  mulc1cncf  23974  cncfcn1  23980  cncfmpt2f  23984  cncfmpt2ss  23985  addccncf  23986  idcncf  23987  sub1cncf  23988  sub2cncf  23989  cdivcncf  23990  negcncf  23991  negfcncf  23992  abscncfALT  23993  cnmpopc  23997  xrhmeo  24015  oprpiece1res1  24020  oprpiece1res2  24021  cnrehmeo  24022  iscau3  24347  caubl  24377  caublcls  24378  evthicc2  24529  ovolre  24594  volsuplem  24624  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  dyadmbllem  24668  volivth  24676  itgfsum  24896  iblabslem  24897  iblabs  24898  bddmulibl  24908  cnlimc  24957  cnlimci  24958  dvcnp2  24989  dvcn  24990  cpnord  25004  cpnres  25006  dvmptntr  25040  dvmptfsum  25044  rolle  25059  dvlipcn  25063  c1liplem1  25065  dvivth  25079  dvfsumabs  25092  ftc1a  25106  ftc1cn  25112  plyssc  25266  plyeq0  25277  0dgr  25311  coemulc  25321  coe0  25322  coesub  25323  coe1termlem  25324  dgrmulc  25337  dgrsub  25338  dvnply2  25352  plycpn  25354  plyremlem  25369  fta1lem  25372  vieta1lem2  25376  aalioulem3  25399  taylthlem1  25437  taylthlem2  25438  ulmcn  25463  psercn  25490  abelth  25505  efcn  25507  efcvx  25513  dvrelog  25697  logcn  25707  dvloglem  25708  dvlog  25711  dvlog2  25713  efopnlem2  25717  logccv  25723  cxpcn  25803  cxpcn3  25806  resqrtcn  25807  sqrtcn  25808  loglesqrt  25816  atancn  25991  jensen  26043  ftalem3  26129  dchrfi  26308  dchrisumlema  26541  pntlem3  26662  uhgrsubgrself  27550  uhgrspansubgr  27561  umgr2adedgwlk  28211  umgr2adedgwlkon  28212  umgr2adedgspth  28214  upgr1wlkdlem2  28411  sspid  28988  ssps  28993  helch  29506  hhssnv  29527  hhsssh  29532  shintcl  29593  chintcl  29595  shlesb1i  29649  omlsi  29667  chlejb1i  29739  chm0i  29753  chabs1  29779  chabs2  29780  spanun  29808  cmidi  29873  pjidmcoi  30440  csmdsymi  30597  sumdmdlem2  30682  dmdbr5ati  30685  mdcompli  30692  dmdcompli  30693  disjdifprg  30815  fcoinver  30847  f1rnen  30865  xppreima  30884  padct  30956  xrinfm  30979  clatp0cl  31156  clatp1cl  31157  xrsp0  31192  xrsp1  31193  cntrcrng  31224  gsumle  31252  cycpmconjslem1  31323  cycpmconjslem2  31324  gsumvsca1  31381  gsumvsca2  31382  qusxpid  31461  ellspds  31466  rspidlid  31472  reff  31691  locfinreflem  31692  esumsnf  31932  esumcvg  31954  sigagenid  32019  iblidicc  32472  cxpcncf1  32475  fdvposlt  32479  fdvneggt  32480  fdvposle  32481  fdvnegge  32482  logdivsqrle  32530  bnj1253  32897  fineqvac  32966  cvmlift2lem6  33170  satfun  33273  mrsubrn  33375  elmrsubrn  33382  elmsubrn  33390  msubrn  33391  onelssex  33563  madebday  34007  imagesset  34182  ivthALT  34451  fness  34465  fneref  34466  refssfne  34474  fnemeet1  34482  fnejoin2  34485  filnetlem2  34495  filnetlem4  34497  ontgval  34547  knoppcnlem10  34609  knoppcnlem11  34610  bj-rabtr  35045  bj-rabtrAUTO  35047  bj-disj2r  35145  bj-restsnid  35185  bj-resta  35194  bj-imdirco  35288  elxp8  35469  finorwe  35480  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfposadd  35751  ftc1cnnclem  35775  ftc1cnnc  35776  ftc1anc  35785  ftc2nc  35786  areacirclem2  35793  areacirclem4  35795  areacirc  35797  caures  35845  constcncf  35847  brssrid  36547  brcnvssrid  36552  refrelid  36566  n0eldmqs  36688  atpsubN  37694  pol1N  37851  dia2dimlem13  39017  dibord  39100  dochvalr  39298  hdmapevec  39776  lcmineqlem10  39974  lcmineqlem12  39976  eqimssd  40111  ismrcd1  40436  ismrc  40439  incssnn0  40449  mzpclall  40465  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  expdioph  40761  aomclem6  40800  kelac1  40804  gicabl  40840  arearect  40962  areaquad  40963  clcnvlem  41120  cnvtrcl0  41123  fvilbd  41186  relexp0a  41213  corcltrcl  41236  clsk1indlem2  41541  ntrclskb  41568  wnefimgd  41661  mnuprdlem4  41782  nzss  41824  lhe4.4ex1a  41836  dvsconst  41837  dvsid  41838  dvsef  41839  binomcxplemnn0  41856  onfrALTlem3  42053  onfrALTlem3VD  42396  unisn0  42491  founiiun0  42617  evthiccabs  42924  climconstmpt  43089  cncfshift  43305  addccncf2  43307  cncfcompt  43314  ioccncflimc  43316  icocncflimc  43320  cncfiooicclem1  43324  cncfiooicc  43325  cncfiooiccre  43326  cxpcncf2  43330  add1cncf  43332  add2cncf  43333  sub1cncfd  43334  sub2cncfd  43335  dvcosre  43343  dvmptfprod  43376  ibliooicc  43402  itgsincmulx  43405  itgsubsticclem  43406  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem16  43554  fourierdlem18  43556  fourierdlem21  43559  fourierdlem22  43560  fourierdlem23  43561  fourierdlem32  43570  fourierdlem33  43571  fourierdlem39  43577  fourierdlem40  43578  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem62  43599  fourierdlem68  43605  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem83  43620  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem93  43630  fourierdlem94  43631  fourierdlem95  43632  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  fouriercn  43663  etransclem18  43683  etransclem22  43687  etransclem34  43699  etransclem46  43711  etransclem47  43712  sge0fsum  43815  meaiininclem  43914  hoidmvlelem2  44024  hspdifhsp  44044  hspmbllem2  44055  hspmbl  44057  iinhoiicclem  44101  pimgtmnf2  44138  smflimsuplem1  44240  smflimsuplem6  44245  srhmsubc  45522  srhmsubcALTV  45540