Theorem ssid 3953

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899

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 3916

This theorem is used by:  ssidd  3954  eqimssd  3987  eqimsscd  3988  eqimssi  3991  eqimss2i  3992  nsspssun  4214  difidALT  4326  inv1  4348  disjpss  4414  disjdif  4426  pwidgOLD  4578  elssuni  4899  unimax  4905  intmin  4928  rintn0  5069  sseliALT  5263  inxpssres  5668  xpss1  5670  xpss2  5671  residm  6001  resdm  6017  resmpt3  6032  cnvrescnv  6187  onelssex  6405  ordunidif  6406  funresfunco  6573  dffn3  6714  fdmrn  6733  fvreseq1  7030  iunpw  7774  onsucuni  7828  tfisi  7859  fparlem3  8114  fparlem4  8115  funsssuppss  8191  tfrlem1  8367  tz7.48-2  8436  oaordi  8538  omwordi  8563  omass  8572  nnaordi  8611  nnmwordi  8628  naddunif  8687  fpmg  8880  boxcutc  8953  domss2  9139  findcard2d  9166  fimax2g  9261  domunfican  9297  fipreima  9331  fimin2g  9475  wofib  9523  wemapso  9529  noinfep  9645  cantnfval2  9654  tcidm  9729  tc0  9730  r1rankidb  9794  r1pw  9840  rankr1id  9859  scott0b  9918  scott0OLD  9919  xpomen  10075  infpwfien  10122  alephsmo  10162  dfac12lem3  10205  cflem  10304  cflecard  10311  cfslb  10325  fin4en1  10368  fin23lem13  10391  fin23lem36  10407  isf32lem1  10412  fin67  10454  dcomex  10506  zorn2lem4  10558  alephexp2  10647  fpwwe2lem12  10708  canthnumlem  10714  wuncidm  10812  eltsk2g  10817  axgroth6  10894  axgroth3  10897  indconst1  12314  xrsup  13988  expcl  14202  hashcard  14479  hashf1lem2  14581  xptrrel  15113  cotrtrclfv  15145  rtrclreclem2  15192  lo1eq  15715  rlimeq  15716  serclim0  15724  isercolllem2  15813  isercoll  15815  fsum2d  15917  fsumabs  15948  fsumrlim  15958  fsumo1  15959  fsumiun  15968  fprod2d  16128  risefaccl  16162  fallfaccl  16163  eflt  16265  rpnnen2lem3  16364  rpnnen2lem5  16366  rpnnen2lem12  16373  rexpen  16376  ressbasssg  17395  ressid  17402  ressinbas  17403  oduclatb  18661  ipopos  18690  fpwipodrs  18694  qusxpid  19375  ghmghmrn  19429  elcntr  19524  cntrnsg  19538  0symgefmndeq  19588  sylow3lem5  19825  lsmss1  19859  lsmss2  19861  cmnbascntr  19999  cntrcmnd  20036  cntrabl  20037  gsumzres  20103  gsumzcl2  20104  gsumzf1o  20106  gsumadd  20117  gsumzmhm  20131  gsumzoppg  20138  dprdf1  20229  ablfac1eulem  20268  gsumle  20339  subrgid  20805  srhmsubc  20912  lbsextlem1  21416  rlmval2  21447  znf1o  21837  zntoslem  21842  css0  21975  uvcresum  22079  frlmlbs  22083  psrass1lem  22221  mdetrsca2  22899  mdetrlin2  22902  mdetunilem5  22911  mdetunilem9  22915  smadiadetglem1  22966  smadiadetglem2  22967  pmatcollpw3  23082  topopn  23204  fiinbas  23250  topbas  23270  topcld  23333  ntrtop  23368  opnneissb  23412  opnssneib  23413  opnneiid  23424  maxlp  23445  isperf2  23450  restperf  23482  idcn  23555  cnconst2  23581  lmres  23598  fiuncmp  23702  1stcelcls  23760  ssref  23811  refref  23812  kgencn2  23856  ptpjpre1  23870  ptbasfi  23880  xkopt  23954  elqtop2  24000  ptcmpfi  24112  fbssfi  24136  opnfbas  24141  filtop  24154  isfil2  24155  isfild  24157  fsubbas  24166  ssfg  24171  filssufilg  24210  ufileu  24218  imaelfm  24250  rnelfm  24252  fmfnfmlem4  24256  neiflim  24273  fclscf  24324  flimfnfcls  24327  tsmsfbas  24427  xpsxmet  24679  xpsdsval  24680  xpsmet  24681  tmsxms  24785  tmsms  24786  imasf1oxms  24788  imasf1oms  24789  prdsxms  24829  prdsms  24830  tmsxpsval  24837  retopbas  25059  cnngp  25078  cnopn  25085  cnperf  25120  retopconn  25129  fsumcn  25171  abscncf  25202  recncf  25203  imcncf  25204  cjcncf  25205  mulc1cncf  25206  cncfcn1  25212  cncfmpt2f  25216  cncfmpt2ss  25217  addccncf  25218  idcncf  25219  sub1cncf  25220  sub2cncf  25221  cdivcncf  25222  negcncf  25223  negfcncf  25224  abscncfALT  25225  cnmpopc  25229  xrhmeo  25247  oprpiece1res1  25252  oprpiece1res2  25253  cnrehmeo  25254  iscau3  25579  caubl  25609  caublcls  25610  mulcncf  25747  evthicc2  25761  ovolre  25826  volsuplem  25856  uniiccdif  25879  uniioovol  25880  uniiccvol  25881  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  dyadmbllem  25900  volivth  25908  itgfsum  26127  iblabslem  26128  iblabs  26129  bddmulibl  26139  cnlimc  26188  cnlimci  26189  dvcnp2  26220  dvcn  26221  cpnord  26235  cpnres  26237  dvmptntr  26271  dvmptfsum  26275  rolle  26290  dvlipcn  26294  c1liplem1  26296  dvivth  26310  dvfsumabs  26323  ftc1a  26337  ftc1cn  26343  plyssc  26498  plyeq0  26510  0dgr  26544  coemulc  26554  coe0  26555  coesub  26556  coe1termlem  26557  dgrmulc  26570  dgrsub  26571  dvnply2  26590  plycpn  26592  plyremlem  26607  fta1lem  26610  vieta1lem2  26616  aalioulem3  26643  taylthlem1  26682  taylthlem2  26683  ulmcn  26708  psercn  26735  abelth  26750  efcn  26752  efcvx  26758  dvrelog  26947  logcn  26957  dvloglem  26958  dvlog  26961  dvlog2  26963  efopnlem2  26967  logccv  26973  cxpcn  27055  cxpcn3  27058  resqrtcn  27059  sqrtcn  27060  loglesqrt  27071  atancn  27246  jensen  27298  ftalem3  27384  dchrfi  27564  dchrisumlema  27797  pntlem3  27918  madebday  28268  expscl  28799  bdaypw2n0bndlem  28831  uhgrsubgrself  29843  uhgrspansubgr  29854  umgr2adedgwlk  30516  umgr2adedgwlkon  30517  umgr2adedgspth  30519  upgr1wlkdlem2  30719  sspid  31309  ssps  31314  helch  31827  hhssnv  31848  hhsssh  31853  shintcl  31914  chintcl  31916  shlesb1i  31970  omlsi  31988  chlejb1i  32060  chm0i  32074  chabs1  32100  chabs2  32101  spanun  32129  cmidi  32194  pjidmcoi  32761  csmdsymi  32918  sumdmdlem2  33003  dmdbr5ati  33006  mdcompli  33013  dmdcompli  33014  disjdifprg  33151  fcoinver  33180  f1rnen  33204  xppreima  33221  padct  33292  xrinfm  33329  clatp0cl  33519  clatp1cl  33520  xrsp0  33555  xrsp1  33556  cntrcrng  33624  cycpmconjslem1  33697  cycpmconjslem2  33698  gsumvsca1  33769  gsumvsca2  33770  ellspds  33906  rspidlid  33912  rlmdim  34224  reff  34453  locfinreflem  34454  esumsnf  34678  esumcvg  34700  sigagenid  34766  iblidicc  35204  cxpcncf1  35207  fdvposlt  35211  fdvneggt  35212  fdvposle  35213  fdvnegge  35214  logdivsqrle  35262  bnj1253  35630  fineqvac  35757  fineqvnttrclse  35765  noinfepfnregs  35773  cvmlift2lem6  36042  satfun  36145  mrsubrn  36247  elmrsubrn  36254  elmsubrn  36262  msubrn  36263  imagesset  36687  nmuladdss  36932  ivthALT  37093  fness  37107  fneref  37108  refssfne  37116  fnemeet1  37124  fnejoin2  37127  filnetlem2  37137  filnetlem4  37139  ontgval  37189  ttctrid  37260  knoppcnlem10  37338  knoppcnlem11  37339  bj-rabtr  37813  bj-rabtrAUTO  37815  bj-disj2r  37911  bj-restsnid  37976  bj-resta  37985  bj-imdirco  38079  elxp8  38262  finorwe  38273  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  mbfposadd  38553  ftc1cnnclem  38577  ftc1cnnc  38578  ftc1anc  38587  ftc2nc  38588  areacirclem2  38595  areacirclem4  38597  areacirc  38599  caures  38662  constcncf  38664  brssrid  39482  brcnvssrid  39487  refrelid  39502  n0eldmqs  39632  atpsubN  40778  pol1N  40935  dia2dimlem13  42101  dibord  42184  dochvalr  42382  hdmapevec  42860  lcmineqlem10  43056  lcmineqlem12  43058  ismrcd1  43662  ismrc  43665  incssnn0  43675  mzpclall  43691  rmydioph  43974  rmxdioph  43976  expdiophlem2  43982  expdioph  43983  aomclem6  44019  kelac1  44023  gicabl  44059  arearect  44175  areaquad  44176  unielid  44179  oege2  44267  oacl2g  44290  ofoaf  44315  clcnvlem  44582  cnvtrcl0  44585  fvilbd  44648  relexp0a  44675  corcltrcl  44698  clsk1indlem2  45001  ntrclskb  45028  wnefimgd  45120  mnuprdlem4  45218  nzss  45260  lhe4.4ex1a  45272  dvsconst  45273  dvsid  45274  dvsef  45275  binomcxplemnn0  45292  onfrALTlem3  45486  onfrALTlem3VD  45828  unisn0  46014  founiiun0  46148  evthiccabs  46452  climconstmpt  46612  cncfshift  46828  addccncf2  46830  cncfcompt  46837  ioccncflimc  46839  icocncflimc  46843  cncfiooicclem1  46847  cncfiooicc  46848  cncfiooiccre  46849  cxpcncf2  46853  add1cncf  46855  add2cncf  46856  sub1cncfd  46857  sub2cncfd  46858  dvcosre  46866  dvmptfprod  46899  ibliooicc  46925  itgsincmulx  46928  itgsubsticclem  46929  itgiccshift  46934  itgperiod  46935  itgsbtaddcnst  46936  dirkeritg  47056  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem16  47077  fourierdlem18  47079  fourierdlem21  47082  fourierdlem22  47083  fourierdlem23  47084  fourierdlem32  47093  fourierdlem33  47094  fourierdlem39  47100  fourierdlem40  47101  fourierdlem57  47117  fourierdlem58  47118  fourierdlem59  47119  fourierdlem62  47122  fourierdlem68  47128  fourierdlem72  47132  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem78  47138  fourierdlem83  47143  fourierdlem84  47144  fourierdlem85  47145  fourierdlem88  47148  fourierdlem93  47153  fourierdlem94  47154  fourierdlem95  47155  fourierdlem97  47157  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  sqwvfoura  47182  sqwvfourb  47183  fouriersw  47185  fouriercn  47186  etransclem18  47206  etransclem22  47210  etransclem34  47222  etransclem46  47234  etransclem47  47235  sge0fsum  47341  meaiininclem  47440  hoidmvlelem2  47550  hspdifhsp  47570  hspmbllem2  47581  hspmbl  47583  iinhoiicclem  47627  pimgtmnf2  47668  smflimsuplem1  47774  smflimsuplem6  47779  cjnpoly  47883  sqrtnpoly  47887  srhmsubcALTV  49366  imaidfu2lem  50161  imaidfu  50162  imaidfu2  50163  setc1onsubc  50654  dvsec  50800  dvcsc  50801  dvcot  50802