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 2121   ⊆ wss 3885

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

This theorem depends on definitions:  df-bi 209  df-ss 3902

This theorem is referenced by:  ssidd  3940  eqimssd  3973  eqimsscd  3974  eqimssi  3977  eqimss2i  3978  nsspssun  4199  difidALT  4308  inv1  4329  disjpss  4392  pwidg  4552  elssuni  4872  unimax  4878  intmin  4901  rintn0  5041  sseliALT  5234  inxpssres  5638  xpss1  5640  xpss2  5641  residm  5969  resdm  5985  resmpt3  5997  cnvrescnv  6150  onelssex  6363  ordunidif  6364  funresfunco  6530  dffn3  6671  fdmrn  6690  fvreseq1  6984  iunpw  7718  onsucuni  7772  tfisi  7803  fparlem3  8057  fparlem4  8058  funsssuppss  8134  tfrlem1  8309  tz7.48-2  8375  oaordi  8475  omwordi  8500  omass  8509  nnaordi  8548  nnmwordi  8565  naddunif  8623  fpmg  8810  boxcutc  8883  domss2  9068  findcard2d  9095  fimax2g  9190  domunfican  9226  fipreima  9262  fimin2g  9406  wofib  9454  wemapso  9460  noinfep  9576  cantnfval2  9585  tcidm  9660  tc0  9661  r1rankidb  9723  r1pw  9764  rankr1id  9781  scott0  9805  xpomen  9932  infpwfien  9979  alephsmo  10019  dfac12lem3  10063  cflem  10162  cflemOLD  10163  cflecard  10170  cfslb  10183  fin4en1  10226  fin23lem13  10249  fin23lem36  10265  isf32lem1  10270  fin67  10312  dcomex  10364  zorn2lem4  10416  alephexp2  10499  fpwwe2lem12  10560  canthnumlem  10566  wuncidm  10664  eltsk2g  10669  axgroth6  10746  axgroth3  10749  indconst1  12167  xrsup  13822  expcl  14036  hashcard  14312  hashf1lem2  14413  xptrrel  14937  cotrtrclfv  14969  rtrclreclem2  15016  lo1eq  15525  rlimeq  15526  serclim0  15534  isercolllem2  15623  isercoll  15625  fsum2d  15728  fsumabs  15759  fsumrlim  15769  fsumo1  15770  fsumiun  15779  fprod2d  15941  risefaccl  15975  fallfaccl  15976  eflt  16079  rpnnen2lem3  16178  rpnnen2lem5  16180  rpnnen2lem12  16187  rexpen  16190  ressbasssg  17202  ressid  17209  ressinbas  17210  oduclatb  18468  ipopos  18497  fpwipodrs  18501  ghmghmrn  19205  elcntr  19300  cntrnsg  19314  0symgefmndeq  19364  sylow3lem5  19601  lsmss1  19635  lsmss2  19637  cmnbascntr  19775  cntrcmnd  19812  cntrabl  19813  gsumzres  19879  gsumzcl2  19880  gsumzf1o  19882  gsumadd  19893  gsumzmhm  19907  gsumzoppg  19914  dprdf1  20005  ablfac1eulem  20044  gsumle  20115  subrgid  20549  srhmsubc  20656  lbsextlem1  21155  rlmval2  21186  znf1o  21530  zntoslem  21535  css0  21668  uvcresum  21772  frlmlbs  21776  psrass1lem  21912  mdetrsca2  22591  mdetrlin2  22594  mdetunilem5  22603  mdetunilem9  22607  smadiadetglem1  22658  smadiadetglem2  22659  pmatcollpw3  22771  topopn  22893  fiinbas  22939  topbas  22959  topcld  23022  ntrtop  23057  opnneissb  23101  opnssneib  23102  opnneiid  23113  maxlp  23134  isperf2  23139  restperf  23171  idcn  23244  cnconst2  23270  lmres  23287  fiuncmp  23391  1stcelcls  23448  ssref  23499  refref  23500  kgencn2  23544  ptpjpre1  23558  ptbasfi  23568  xkopt  23642  elqtop2  23688  ptcmpfi  23800  fbssfi  23824  opnfbas  23829  filtop  23842  isfil2  23843  isfild  23845  fsubbas  23854  ssfg  23859  filssufilg  23898  ufileu  23906  imaelfm  23938  rnelfm  23940  fmfnfmlem4  23944  neiflim  23961  fclscf  24012  flimfnfcls  24015  tsmsfbas  24115  xpsxmet  24367  xpsdsval  24368  xpsmet  24369  tmsxms  24473  tmsms  24474  imasf1oxms  24476  imasf1oms  24477  prdsxms  24517  prdsms  24518  tmsxpsval  24525  retopbas  24747  cnngp  24766  cnopn  24773  cnperf  24808  retopconn  24817  fsumcn  24859  abscncf  24890  recncf  24891  imcncf  24892  cjcncf  24893  mulc1cncf  24894  cncfcn1  24900  cncfmpt2f  24904  cncfmpt2ss  24905  addccncf  24906  idcncf  24907  sub1cncf  24908  sub2cncf  24909  cdivcncf  24910  negcncf  24911  negfcncf  24912  abscncfALT  24913  cnmpopc  24917  xrhmeo  24935  oprpiece1res1  24940  oprpiece1res2  24941  cnrehmeo  24942  iscau3  25267  caubl  25297  caublcls  25298  mulcncf  25435  evthicc2  25449  ovolre  25514  volsuplem  25544  uniiccdif  25567  uniioovol  25568  uniiccvol  25569  uniioombllem3  25574  uniioombllem4  25575  uniioombllem5  25576  dyadmbllem  25588  volivth  25596  itgfsum  25816  iblabslem  25817  iblabs  25818  bddmulibl  25828  cnlimc  25877  cnlimci  25878  dvcnp2  25909  dvcn  25910  cpnord  25924  cpnres  25926  dvmptntr  25960  dvmptfsum  25964  rolle  25979  dvlipcn  25983  c1liplem1  25985  dvivth  25999  dvfsumabs  26012  ftc1a  26026  ftc1cn  26032  plyssc  26187  plyeq0  26198  0dgr  26232  coemulc  26242  coe0  26243  coesub  26244  coe1termlem  26245  dgrmulc  26258  dgrsub  26259  dvnply2  26275  plycpn  26277  plyremlem  26292  fta1lem  26295  vieta1lem2  26299  aalioulem3  26322  taylthlem1  26360  taylthlem2  26361  ulmcn  26386  psercn  26413  abelth  26428  efcn  26430  efcvx  26436  dvrelog  26623  logcn  26633  dvloglem  26634  dvlog  26637  dvlog2  26639  efopnlem2  26643  logccv  26649  cxpcn  26731  cxpcn3  26734  resqrtcn  26735  sqrtcn  26736  loglesqrt  26747  atancn  26922  jensen  26974  ftalem3  27060  dchrfi  27240  dchrisumlema  27473  pntlem3  27594  madebday  27914  expscl  28445  bdaypw2n0bndlem  28477  uhgrsubgrself  29371  uhgrspansubgr  29382  umgr2adedgwlk  30035  umgr2adedgwlkon  30036  umgr2adedgspth  30038  upgr1wlkdlem2  30238  sspid  30818  ssps  30823  helch  31336  hhssnv  31357  hhsssh  31362  shintcl  31423  chintcl  31425  shlesb1i  31479  omlsi  31497  chlejb1i  31569  chm0i  31583  chabs1  31609  chabs2  31610  spanun  31638  cmidi  31703  pjidmcoi  32270  csmdsymi  32427  sumdmdlem2  32512  dmdbr5ati  32515  mdcompli  32522  dmdcompli  32523  disjdifprg  32668  fcoinver  32697  f1rnen  32724  xppreima  32741  padct  32814  xrinfm  32851  clatp0cl  33059  clatp1cl  33060  xrsp0  33095  xrsp1  33096  cntrcrng  33166  cycpmconjslem1  33239  cycpmconjslem2  33240  gsumvsca1  33311  gsumvsca2  33312  qusxpid  33450  ellspds  33455  rspidlid  33462  rlmdim  33806  reff  34035  locfinreflem  34036  esumsnf  34260  esumcvg  34282  sigagenid  34347  iblidicc  34788  cxpcncf1  34791  fdvposlt  34795  fdvneggt  34796  fdvposle  34797  fdvnegge  34798  logdivsqrle  34846  bnj1253  35214  fineqvac  35312  fineqvnttrclse  35320  noinfepfnregs  35328  cvmlift2lem6  35551  satfun  35654  mrsubrn  35756  elmrsubrn  35763  elmsubrn  35771  msubrn  35772  imagesset  36196  ivthALT  36578  fness  36592  fneref  36593  refssfne  36601  fnemeet1  36609  fnejoin2  36612  filnetlem2  36622  filnetlem4  36624  ontgval  36674  ttctrid  36745  knoppcnlem10  36823  knoppcnlem11  36824  bj-rabtr  37298  bj-rabtrAUTO  37300  bj-disj2r  37396  bj-restsnid  37460  bj-resta  37469  bj-imdirco  37565  elxp8  37748  finorwe  37759  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  ovoliunnfl  38044  voliunnfl  38046  volsupnfl  38047  mbfposadd  38049  ftc1cnnclem  38073  ftc1cnnc  38074  ftc1anc  38083  ftc2nc  38084  areacirclem2  38091  areacirclem4  38093  areacirc  38095  caures  38142  constcncf  38144  brssrid  38964  brcnvssrid  38969  refrelid  38984  n0eldmqs  39114  atpsubN  40260  pol1N  40417  dia2dimlem13  41583  dibord  41666  dochvalr  41864  hdmapevec  42342  lcmineqlem10  42538  lcmineqlem12  42540  ismrcd1  43162  ismrc  43165  incssnn0  43175  mzpclall  43191  rmydioph  43474  rmxdioph  43476  expdiophlem2  43482  expdioph  43483  aomclem6  43519  kelac1  43523  gicabl  43559  arearect  43675  areaquad  43676  unielid  43679  oege2  43767  oacl2g  43790  ofoaf  43815  clcnvlem  44082  cnvtrcl0  44085  fvilbd  44148  relexp0a  44175  corcltrcl  44198  clsk1indlem2  44501  ntrclskb  44528  wnefimgd  44620  mnuprdlem4  44734  nzss  44776  lhe4.4ex1a  44788  dvsconst  44789  dvsid  44790  dvsef  44791  binomcxplemnn0  44808  onfrALTlem3  45003  onfrALTlem3VD  45345  unisn0  45517  founiiun0  45651  evthiccabs  45955  climconstmpt  46115  cncfshift  46331  addccncf2  46333  cncfcompt  46340  ioccncflimc  46342  icocncflimc  46346  cncfiooicclem1  46350  cncfiooicc  46351  cncfiooiccre  46352  cxpcncf2  46356  add1cncf  46358  add2cncf  46359  sub1cncfd  46360  sub2cncfd  46361  dvcosre  46369  dvmptfprod  46402  ibliooicc  46428  itgsincmulx  46431  itgsubsticclem  46432  itgiccshift  46437  itgperiod  46438  itgsbtaddcnst  46439  dirkeritg  46559  dirkercncflem2  46561  dirkercncflem4  46563  fourierdlem16  46580  fourierdlem18  46582  fourierdlem21  46585  fourierdlem22  46586  fourierdlem23  46587  fourierdlem32  46596  fourierdlem33  46597  fourierdlem39  46603  fourierdlem40  46604  fourierdlem57  46620  fourierdlem58  46621  fourierdlem59  46622  fourierdlem62  46625  fourierdlem68  46631  fourierdlem72  46635  fourierdlem73  46636  fourierdlem74  46637  fourierdlem75  46638  fourierdlem76  46639  fourierdlem78  46641  fourierdlem83  46646  fourierdlem84  46647  fourierdlem85  46648  fourierdlem88  46651  fourierdlem93  46656  fourierdlem94  46657  fourierdlem95  46658  fourierdlem97  46660  fourierdlem101  46664  fourierdlem103  46666  fourierdlem104  46667  fourierdlem111  46674  fourierdlem112  46675  fourierdlem113  46676  sqwvfoura  46685  sqwvfourb  46686  fouriersw  46688  fouriercn  46689  etransclem18  46709  etransclem22  46713  etransclem34  46725  etransclem46  46737  etransclem47  46738  sge0fsum  46844  meaiininclem  46943  hoidmvlelem2  47053  hspdifhsp  47073  hspmbllem2  47084  hspmbl  47086  iinhoiicclem  47130  pimgtmnf2  47171  smflimsuplem1  47277  smflimsuplem6  47282  cjnpoly  47366  srhmsubcALTV  48830  imaidfu2lem  49613  imaidfu  49614  imaidfu2  49615  setc1onsubc  50106