Theorem ssid 3981

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3926

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

This theorem depends on definitions:  df-bi 207  df-ss 3943

This theorem is referenced by:  ssidd  3982  eqimssd  4015  eqimsscd  4016  eqimssi  4019  eqimss2i  4020  nsspssun  4243  difidALT  4352  inv1  4373  disjpss  4436  pwidg  4595  elssuni  4913  unimax  4920  intmin  4944  rintn0  5085  sseliALT  5279  inxpssres  5671  xpss1  5673  xpss2  5674  residm  5997  resdm  6013  resmpt3  6025  cnvrescnv  6184  onelssex  6401  ordunidif  6402  funresfunco  6576  dffn3  6717  fdmrn  6736  fvreseq1  7028  iunpw  7763  onsucuni  7820  tfisi  7852  fparlem3  8111  fparlem4  8112  funsssuppss  8187  tfrlem1  8388  tz7.48-2  8454  oaordi  8556  omwordi  8581  omass  8590  nnaordi  8628  nnmwordi  8645  naddunif  8703  fpmg  8880  boxcutc  8953  domss2  9148  findcard2d  9178  0finOLD  9182  en1eqsnOLD  9279  fimax2g  9292  domunfican  9331  fipreima  9368  fimin2g  9509  wofib  9557  wemapso  9563  noinfep  9672  cantnfval2  9681  tcidm  9758  tc0  9759  r1rankidb  9816  r1pw  9857  rankr1id  9874  scott0  9898  xpomen  10027  infpwfien  10074  alephsmo  10114  dfac12lem3  10158  cflem  10257  cflemOLD  10258  cflecard  10265  cfslb  10278  fin4en1  10321  fin23lem13  10344  fin23lem36  10360  isf32lem1  10365  fin67  10407  dcomex  10459  zorn2lem4  10511  alephexp2  10593  fpwwe2lem12  10654  canthnumlem  10660  wuncidm  10758  eltsk2g  10763  axgroth6  10840  axgroth3  10843  xrsup  13883  expcl  14095  hashcard  14371  hashf1lem2  14472  xptrrel  14997  cotrtrclfv  15029  rtrclreclem2  15076  lo1eq  15582  rlimeq  15583  serclim0  15591  isercolllem2  15680  isercoll  15682  fsum2d  15785  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  fprod2d  15995  risefaccl  16029  fallfaccl  16030  eflt  16133  rpnnen2lem3  16232  rpnnen2lem5  16234  rpnnen2lem12  16241  rexpen  16244  ressbasssg  17256  ressid  17263  ressinbas  17264  oduclatb  18515  ipopos  18544  fpwipodrs  18548  ghmghmrn  19216  elcntr  19311  cntrnsg  19325  0symgefmndeq  19373  sylow3lem5  19610  lsmss1  19644  lsmss2  19646  cmnbascntr  19784  cntrcmnd  19821  cntrabl  19822  gsumzres  19888  gsumzcl2  19889  gsumzf1o  19891  gsumadd  19902  gsumzmhm  19916  gsumzoppg  19923  dprdf1  20014  ablfac1eulem  20053  subrgid  20531  srhmsubc  20638  lbsextlem1  21117  rlmval2  21148  znf1o  21510  zntoslem  21515  css0  21647  uvcresum  21751  frlmlbs  21755  psrass1lem  21890  mdetrsca2  22540  mdetrlin2  22543  mdetunilem5  22552  mdetunilem9  22556  smadiadetglem1  22607  smadiadetglem2  22608  pmatcollpw3  22720  topopn  22842  fiinbas  22888  topbas  22908  topcld  22971  ntrtop  23006  opnneissb  23050  opnssneib  23051  opnneiid  23062  maxlp  23083  isperf2  23088  restperf  23120  idcn  23193  cnconst2  23219  lmres  23236  fiuncmp  23340  1stcelcls  23397  ssref  23448  refref  23449  kgencn2  23493  ptpjpre1  23507  ptbasfi  23517  xkopt  23591  elqtop2  23637  ptcmpfi  23749  fbssfi  23773  opnfbas  23778  filtop  23791  isfil2  23792  isfild  23794  fsubbas  23803  ssfg  23808  filssufilg  23847  ufileu  23855  imaelfm  23887  rnelfm  23889  fmfnfmlem4  23893  neiflim  23910  fclscf  23961  flimfnfcls  23964  tsmsfbas  24064  xpsxmet  24317  xpsdsval  24318  xpsmet  24319  tmsxms  24423  tmsms  24424  imasf1oxms  24426  imasf1oms  24427  prdsxms  24467  prdsms  24468  tmsxpsval  24475  retopbas  24697  cnngp  24716  cnopn  24723  cnperf  24758  retopconn  24767  fsumcn  24810  abscncf  24843  recncf  24844  imcncf  24845  cjcncf  24846  mulc1cncf  24847  cncfcn1  24853  cncfmpt2f  24857  cncfmpt2ss  24858  addccncf  24859  idcncf  24860  sub1cncf  24861  sub2cncf  24862  cdivcncf  24863  negcncf  24864  negcncfOLD  24865  negfcncf  24866  abscncfALT  24867  cnmpopc  24871  xrhmeo  24893  oprpiece1res1  24898  oprpiece1res2  24899  cnrehmeo  24900  cnrehmeoOLD  24901  iscau3  25228  caubl  25258  caublcls  25259  mulcncf  25396  evthicc2  25411  ovolre  25476  volsuplem  25506  uniiccdif  25529  uniioovol  25530  uniiccvol  25531  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  dyadmbllem  25550  volivth  25558  itgfsum  25778  iblabslem  25779  iblabs  25780  bddmulibl  25790  cnlimc  25839  cnlimci  25840  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  cpnord  25887  cpnres  25889  dvmptntr  25925  dvmptfsum  25929  rolle  25944  dvlipcn  25949  c1liplem1  25951  dvivth  25965  dvfsumabs  25979  ftc1a  25994  ftc1cn  26000  plyssc  26155  plyeq0  26166  0dgr  26200  coemulc  26210  coe0  26211  coesub  26212  coe1termlem  26213  dgrmulc  26227  dgrsub  26228  dvnply2  26245  plycpn  26247  plyremlem  26262  fta1lem  26265  vieta1lem2  26269  aalioulem3  26292  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmcn  26358  psercn  26386  abelth  26401  efcn  26403  efcvx  26409  dvrelog  26596  logcn  26606  dvloglem  26607  dvlog  26610  dvlog2  26612  efopnlem2  26616  logccv  26622  cxpcn  26704  cxpcnOLD  26705  cxpcn3  26708  resqrtcn  26709  sqrtcn  26710  loglesqrt  26721  atancn  26896  jensen  26949  ftalem3  27035  dchrfi  27216  dchrisumlema  27449  pntlem3  27570  madebday  27855  uhgrsubgrself  29205  uhgrspansubgr  29216  umgr2adedgwlk  29873  umgr2adedgwlkon  29874  umgr2adedgspth  29876  upgr1wlkdlem2  30073  sspid  30652  ssps  30657  helch  31170  hhssnv  31191  hhsssh  31196  shintcl  31257  chintcl  31259  shlesb1i  31313  omlsi  31331  chlejb1i  31403  chm0i  31417  chabs1  31443  chabs2  31444  spanun  31472  cmidi  31537  pjidmcoi  32104  csmdsymi  32261  sumdmdlem2  32346  dmdbr5ati  32349  mdcompli  32356  dmdcompli  32357  disjdifprg  32502  fcoinver  32531  f1rnen  32553  xppreima  32569  padct  32643  xrinfm  32678  clatp0cl  32902  clatp1cl  32903  xrsp0  32950  xrsp1  32951  cntrcrng  33010  gsumle  33038  cycpmconjslem1  33111  cycpmconjslem2  33112  gsumvsca1  33169  gsumvsca2  33170  qusxpid  33324  ellspds  33329  rspidlid  33336  rlmdim  33595  reff  33816  locfinreflem  33817  esumsnf  34041  esumcvg  34063  sigagenid  34128  iblidicc  34570  cxpcncf1  34573  fdvposlt  34577  fdvneggt  34578  fdvposle  34579  fdvnegge  34580  logdivsqrle  34628  bnj1253  34994  fineqvac  35074  cvmlift2lem6  35276  satfun  35379  mrsubrn  35481  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  imagesset  35917  ivthALT  36299  fness  36313  fneref  36314  refssfne  36322  fnemeet1  36330  fnejoin2  36333  filnetlem2  36343  filnetlem4  36345  ontgval  36395  knoppcnlem10  36466  knoppcnlem11  36467  bj-rabtr  36894  bj-rabtrAUTO  36896  bj-disj2r  36992  bj-restsnid  37051  bj-resta  37060  bj-imdirco  37154  elxp8  37335  finorwe  37346  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfposadd  37637  ftc1cnnclem  37661  ftc1cnnc  37662  ftc1anc  37671  ftc2nc  37672  areacirclem2  37679  areacirclem4  37681  areacirc  37683  caures  37730  constcncf  37732  brssrid  38466  brcnvssrid  38471  refrelid  38486  n0eldmqs  38612  atpsubN  39718  pol1N  39875  dia2dimlem13  41041  dibord  41124  dochvalr  41322  hdmapevec  41800  lcmineqlem10  41997  lcmineqlem12  41999  ismrcd1  42668  ismrc  42671  incssnn0  42681  mzpclall  42697  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  aomclem6  43030  kelac1  43034  gicabl  43070  arearect  43186  areaquad  43187  unielid  43190  oege2  43278  oacl2g  43301  ofoaf  43326  clcnvlem  43594  cnvtrcl0  43597  fvilbd  43660  relexp0a  43687  corcltrcl  43710  clsk1indlem2  44013  ntrclskb  44040  wnefimgd  44132  mnuprdlem4  44247  nzss  44289  lhe4.4ex1a  44301  dvsconst  44302  dvsid  44303  dvsef  44304  binomcxplemnn0  44321  onfrALTlem3  44517  onfrALTlem3VD  44859  unisn0  45026  founiiun0  45162  evthiccabs  45473  climconstmpt  45635  cncfshift  45851  addccncf2  45853  cncfcompt  45860  ioccncflimc  45862  icocncflimc  45866  cncfiooicclem1  45870  cncfiooicc  45871  cncfiooiccre  45872  cxpcncf2  45876  add1cncf  45878  add2cncf  45879  sub1cncfd  45880  sub2cncfd  45881  dvcosre  45889  dvmptfprod  45922  ibliooicc  45948  itgsincmulx  45951  itgsubsticclem  45952  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem16  46100  fourierdlem18  46102  fourierdlem21  46105  fourierdlem22  46106  fourierdlem23  46107  fourierdlem32  46116  fourierdlem33  46117  fourierdlem39  46123  fourierdlem40  46124  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem62  46145  fourierdlem68  46151  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem93  46176  fourierdlem94  46177  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  fouriercn  46209  etransclem18  46229  etransclem22  46233  etransclem34  46245  etransclem46  46257  etransclem47  46258  sge0fsum  46364  meaiininclem  46463  hoidmvlelem2  46573  hspdifhsp  46593  hspmbllem2  46604  hspmbl  46606  iinhoiicclem  46650  pimgtmnf2  46691  smflimsuplem1  46797  smflimsuplem6  46802  srhmsubcALTV  48248  imaidfu2lem  49016  imaidfu  49017  imaidfu2  49018  setc1onsubc  49427