Theorem ssid 3956

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

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

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 3919

This theorem is used by:  ssidd  3957  eqimssd  3990  eqimsscd  3991  eqimssi  3994  eqimss2i  3995  nsspssun  4217  difidALT  4329  inv1  4351  disjpss  4417  disjdif  4429  pwidgOLD  4581  elssuni  4902  unimax  4908  intmin  4931  rintn0  5073  sseliALT  5270  inxpssres  5676  xpss1  5678  xpss2  5679  residm  6007  resdm  6023  resmpt3  6038  cnvrescnv  6193  onelssex  6411  ordunidif  6412  funresfunco  6578  dffn3  6719  fdmrn  6738  fvreseq1  7035  iunpw  7774  onsucuni  7828  tfisi  7859  fparlem3  8115  fparlem4  8116  funsssuppss  8192  tfrlem1  8368  tz7.48-2  8435  oaordi  8537  omwordi  8562  omass  8571  nnaordi  8610  nnmwordi  8627  naddunif  8686  fpmg  8879  boxcutc  8952  domss2  9138  findcard2d  9165  fimax2g  9260  domunfican  9295  fipreima  9329  fimin2g  9473  wofib  9521  wemapso  9527  noinfep  9643  cantnfval2  9652  tcidm  9727  tc0  9728  r1rankidb  9790  r1pw  9831  rankr1id  9848  scott0b  9880  scott0OLD  9881  xpomen  10022  infpwfien  10069  alephsmo  10109  dfac12lem3  10152  cflem  10251  cflecard  10258  cfslb  10272  fin4en1  10315  fin23lem13  10338  fin23lem36  10354  isf32lem1  10359  fin67  10401  dcomex  10453  zorn2lem4  10505  alephexp2  10594  fpwwe2lem12  10655  canthnumlem  10661  wuncidm  10759  eltsk2g  10764  axgroth6  10841  axgroth3  10844  indconst1  12259  xrsup  13933  expcl  14147  hashcard  14423  hashf1lem2  14525  xptrrel  15057  cotrtrclfv  15089  rtrclreclem2  15136  lo1eq  15659  rlimeq  15660  serclim0  15668  isercolllem2  15757  isercoll  15759  fsum2d  15861  fsumabs  15892  fsumrlim  15902  fsumo1  15903  fsumiun  15912  fprod2d  16074  risefaccl  16108  fallfaccl  16109  eflt  16211  rpnnen2lem3  16310  rpnnen2lem5  16312  rpnnen2lem12  16319  rexpen  16322  ressbasssg  17335  ressid  17342  ressinbas  17343  oduclatb  18601  ipopos  18630  fpwipodrs  18634  qusxpid  19314  ghmghmrn  19368  elcntr  19463  cntrnsg  19477  0symgefmndeq  19527  sylow3lem5  19764  lsmss1  19798  lsmss2  19800  cmnbascntr  19938  cntrcmnd  19975  cntrabl  19976  gsumzres  20042  gsumzcl2  20043  gsumzf1o  20045  gsumadd  20056  gsumzmhm  20070  gsumzoppg  20077  dprdf1  20168  ablfac1eulem  20207  gsumle  20278  subrgid  20741  srhmsubc  20848  lbsextlem1  21351  rlmval2  21382  znf1o  21770  zntoslem  21775  css0  21908  uvcresum  22012  frlmlbs  22016  psrass1lem  22154  mdetrsca2  22832  mdetrlin2  22835  mdetunilem5  22844  mdetunilem9  22848  smadiadetglem1  22899  smadiadetglem2  22900  pmatcollpw3  23015  topopn  23137  fiinbas  23183  topbas  23203  topcld  23266  ntrtop  23301  opnneissb  23345  opnssneib  23346  opnneiid  23357  maxlp  23378  isperf2  23383  restperf  23415  idcn  23488  cnconst2  23514  lmres  23531  fiuncmp  23635  1stcelcls  23693  ssref  23744  refref  23745  kgencn2  23789  ptpjpre1  23803  ptbasfi  23813  xkopt  23887  elqtop2  23933  ptcmpfi  24045  fbssfi  24069  opnfbas  24074  filtop  24087  isfil2  24088  isfild  24090  fsubbas  24099  ssfg  24104  filssufilg  24143  ufileu  24151  imaelfm  24183  rnelfm  24185  fmfnfmlem4  24189  neiflim  24206  fclscf  24257  flimfnfcls  24260  tsmsfbas  24360  xpsxmet  24612  xpsdsval  24613  xpsmet  24614  tmsxms  24718  tmsms  24719  imasf1oxms  24721  imasf1oms  24722  prdsxms  24762  prdsms  24763  tmsxpsval  24770  retopbas  24992  cnngp  25011  cnopn  25018  cnperf  25053  retopconn  25062  fsumcn  25104  abscncf  25135  recncf  25136  imcncf  25137  cjcncf  25138  mulc1cncf  25139  cncfcn1  25145  cncfmpt2f  25149  cncfmpt2ss  25150  addccncf  25151  idcncf  25152  sub1cncf  25153  sub2cncf  25154  cdivcncf  25155  negcncf  25156  negfcncf  25157  abscncfALT  25158  cnmpopc  25162  xrhmeo  25180  oprpiece1res1  25185  oprpiece1res2  25186  cnrehmeo  25187  iscau3  25512  caubl  25542  caublcls  25543  mulcncf  25680  evthicc2  25694  ovolre  25759  volsuplem  25789  uniiccdif  25812  uniioovol  25813  uniiccvol  25814  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  dyadmbllem  25833  volivth  25841  itgfsum  26061  iblabslem  26062  iblabs  26063  bddmulibl  26073  cnlimc  26122  cnlimci  26123  dvcnp2  26154  dvcn  26155  cpnord  26169  cpnres  26171  dvmptntr  26205  dvmptfsum  26209  rolle  26224  dvlipcn  26228  c1liplem1  26230  dvivth  26244  dvfsumabs  26257  ftc1a  26271  ftc1cn  26277  plyssc  26432  plyeq0  26444  0dgr  26478  coemulc  26488  coe0  26489  coesub  26490  coe1termlem  26491  dgrmulc  26504  dgrsub  26505  dvnply2  26524  plycpn  26526  plyremlem  26541  fta1lem  26544  vieta1lem2  26550  aalioulem3  26577  taylthlem1  26616  taylthlem2  26617  ulmcn  26642  psercn  26669  abelth  26684  efcn  26686  efcvx  26692  dvrelog  26882  logcn  26892  dvloglem  26893  dvlog  26896  dvlog2  26898  efopnlem2  26902  logccv  26908  cxpcn  26990  cxpcn3  26993  resqrtcn  26994  sqrtcn  26995  loglesqrt  27006  atancn  27181  jensen  27233  ftalem3  27319  dchrfi  27499  dchrisumlema  27732  pntlem3  27853  madebday  28173  expscl  28704  bdaypw2n0bndlem  28736  uhgrsubgrself  29748  uhgrspansubgr  29759  umgr2adedgwlk  30421  umgr2adedgwlkon  30422  umgr2adedgspth  30424  upgr1wlkdlem2  30624  sspid  31214  ssps  31219  helch  31732  hhssnv  31753  hhsssh  31758  shintcl  31819  chintcl  31821  shlesb1i  31875  omlsi  31893  chlejb1i  31965  chm0i  31979  chabs1  32005  chabs2  32006  spanun  32034  cmidi  32099  pjidmcoi  32666  csmdsymi  32823  sumdmdlem2  32908  dmdbr5ati  32911  mdcompli  32918  dmdcompli  32919  disjdifprg  33056  fcoinver  33085  f1rnen  33109  xppreima  33126  padct  33197  xrinfm  33234  clatp0cl  33424  clatp1cl  33425  xrsp0  33460  xrsp1  33461  cntrcrng  33529  cycpmconjslem1  33602  cycpmconjslem2  33603  gsumvsca1  33674  gsumvsca2  33675  ellspds  33811  rspidlid  33817  rlmdim  34128  reff  34357  locfinreflem  34358  esumsnf  34582  esumcvg  34604  sigagenid  34670  iblidicc  35108  cxpcncf1  35111  fdvposlt  35115  fdvneggt  35116  fdvposle  35117  fdvnegge  35118  logdivsqrle  35166  bnj1253  35534  fineqvac  35650  fineqvnttrclse  35658  noinfepfnregs  35666  cvmlift2lem6  35895  satfun  35998  mrsubrn  36100  elmrsubrn  36107  elmsubrn  36115  msubrn  36116  imagesset  36540  nmuladdss  36801  ivthALT  36962  fness  36976  fneref  36977  refssfne  36985  fnemeet1  36993  fnejoin2  36996  filnetlem2  37006  filnetlem4  37008  ontgval  37058  ttctrid  37129  knoppcnlem10  37207  knoppcnlem11  37208  bj-rabtr  37682  bj-rabtrAUTO  37684  bj-disj2r  37780  bj-restsnid  37845  bj-resta  37854  bj-imdirco  37950  elxp8  38133  finorwe  38144  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  mbfposadd  38424  ftc1cnnclem  38448  ftc1cnnc  38449  ftc1anc  38458  ftc2nc  38459  areacirclem2  38466  areacirclem4  38468  areacirc  38470  caures  38518  constcncf  38520  brssrid  39338  brcnvssrid  39343  refrelid  39358  n0eldmqs  39488  atpsubN  40634  pol1N  40791  dia2dimlem13  41957  dibord  42040  dochvalr  42238  hdmapevec  42716  lcmineqlem10  42912  lcmineqlem12  42914  ismrcd1  43551  ismrc  43554  incssnn0  43564  mzpclall  43580  rmydioph  43863  rmxdioph  43865  expdiophlem2  43871  expdioph  43872  aomclem6  43908  kelac1  43912  gicabl  43948  arearect  44064  areaquad  44065  unielid  44068  oege2  44156  oacl2g  44179  ofoaf  44204  clcnvlem  44471  cnvtrcl0  44474  fvilbd  44537  relexp0a  44564  corcltrcl  44587  clsk1indlem2  44890  ntrclskb  44917  wnefimgd  45009  mnuprdlem4  45107  nzss  45149  lhe4.4ex1a  45161  dvsconst  45162  dvsid  45163  dvsef  45164  binomcxplemnn0  45181  onfrALTlem3  45375  onfrALTlem3VD  45717  unisn0  45896  founiiun0  46030  evthiccabs  46334  climconstmpt  46494  cncfshift  46710  addccncf2  46712  cncfcompt  46719  ioccncflimc  46721  icocncflimc  46725  cncfiooicclem1  46729  cncfiooicc  46730  cncfiooiccre  46731  cxpcncf2  46735  add1cncf  46737  add2cncf  46738  sub1cncfd  46739  sub2cncfd  46740  dvcosre  46748  dvmptfprod  46781  ibliooicc  46807  itgsincmulx  46810  itgsubsticclem  46811  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  dirkeritg  46938  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem16  46959  fourierdlem18  46961  fourierdlem21  46964  fourierdlem22  46965  fourierdlem23  46966  fourierdlem32  46975  fourierdlem33  46976  fourierdlem39  46982  fourierdlem40  46983  fourierdlem57  46999  fourierdlem58  47000  fourierdlem59  47001  fourierdlem62  47004  fourierdlem68  47010  fourierdlem72  47014  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem78  47020  fourierdlem83  47025  fourierdlem84  47026  fourierdlem85  47027  fourierdlem88  47030  fourierdlem93  47035  fourierdlem94  47036  fourierdlem95  47037  fourierdlem97  47039  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  fouriercn  47068  etransclem18  47088  etransclem22  47092  etransclem34  47104  etransclem46  47116  etransclem47  47117  sge0fsum  47223  meaiininclem  47322  hoidmvlelem2  47432  hspdifhsp  47452  hspmbllem2  47463  hspmbl  47465  iinhoiicclem  47509  pimgtmnf2  47550  smflimsuplem1  47656  smflimsuplem6  47661  cjnpoly  47765  sqrtnpoly  47769  srhmsubcALTV  49248  imaidfu2lem  50043  imaidfu  50044  imaidfu2  50045  setc1onsubc  50536  dvsec  50697  dvcsc  50698  dvcot  50699