Theorem ssid 3958

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3903

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 3920

This theorem is referenced by:  ssidd  3959  eqimssd  3992  eqimsscd  3993  eqimssi  3996  eqimss2i  3997  nsspssun  4219  difidALT  4328  inv1  4349  disjpss  4412  pwidg  4571  elssuni  4888  unimax  4894  intmin  4918  rintn0  5058  sseliALT  5248  inxpssres  5636  xpss1  5638  xpss2  5639  residm  5961  resdm  5977  resmpt3  5989  cnvrescnv  6144  onelssex  6356  ordunidif  6357  funresfunco  6523  dffn3  6664  fdmrn  6683  fvreseq1  6973  iunpw  7707  onsucuni  7761  tfisi  7792  fparlem3  8047  fparlem4  8048  funsssuppss  8123  tfrlem1  8298  tz7.48-2  8364  oaordi  8464  omwordi  8489  omass  8498  nnaordi  8536  nnmwordi  8553  naddunif  8611  fpmg  8795  boxcutc  8868  domss2  9053  findcard2d  9080  0finOLD  9084  fimax2g  9175  domunfican  9211  fipreima  9248  fimin2g  9389  wofib  9437  wemapso  9443  noinfep  9556  cantnfval2  9565  tcidm  9642  tc0  9643  r1rankidb  9700  r1pw  9741  rankr1id  9758  scott0  9782  xpomen  9909  infpwfien  9956  alephsmo  9996  dfac12lem3  10040  cflem  10139  cflemOLD  10140  cflecard  10147  cfslb  10160  fin4en1  10203  fin23lem13  10226  fin23lem36  10242  isf32lem1  10247  fin67  10289  dcomex  10341  zorn2lem4  10393  alephexp2  10475  fpwwe2lem12  10536  canthnumlem  10542  wuncidm  10640  eltsk2g  10645  axgroth6  10722  axgroth3  10725  xrsup  13772  expcl  13986  hashcard  14262  hashf1lem2  14363  xptrrel  14887  cotrtrclfv  14919  rtrclreclem2  14966  lo1eq  15475  rlimeq  15476  serclim0  15484  isercolllem2  15573  isercoll  15575  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  fprod2d  15888  risefaccl  15922  fallfaccl  15923  eflt  16026  rpnnen2lem3  16125  rpnnen2lem5  16127  rpnnen2lem12  16134  rexpen  16137  ressbasssg  17148  ressid  17155  ressinbas  17156  oduclatb  18413  ipopos  18442  fpwipodrs  18446  ghmghmrn  19114  elcntr  19209  cntrnsg  19223  0symgefmndeq  19273  sylow3lem5  19510  lsmss1  19544  lsmss2  19546  cmnbascntr  19684  cntrcmnd  19721  cntrabl  19722  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumadd  19802  gsumzmhm  19816  gsumzoppg  19823  dprdf1  19914  ablfac1eulem  19953  gsumle  20024  subrgid  20458  srhmsubc  20565  lbsextlem1  21065  rlmval2  21096  znf1o  21458  zntoslem  21463  css0  21596  uvcresum  21700  frlmlbs  21704  psrass1lem  21839  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  mdetunilem9  22505  smadiadetglem1  22556  smadiadetglem2  22557  pmatcollpw3  22669  topopn  22791  fiinbas  22837  topbas  22857  topcld  22920  ntrtop  22955  opnneissb  22999  opnssneib  23000  opnneiid  23011  maxlp  23032  isperf2  23037  restperf  23069  idcn  23142  cnconst2  23168  lmres  23185  fiuncmp  23289  1stcelcls  23346  ssref  23397  refref  23398  kgencn2  23442  ptpjpre1  23456  ptbasfi  23466  xkopt  23540  elqtop2  23586  ptcmpfi  23698  fbssfi  23722  opnfbas  23727  filtop  23740  isfil2  23741  isfild  23743  fsubbas  23752  ssfg  23757  filssufilg  23796  ufileu  23804  imaelfm  23836  rnelfm  23838  fmfnfmlem4  23842  neiflim  23859  fclscf  23910  flimfnfcls  23913  tsmsfbas  24013  xpsxmet  24266  xpsdsval  24267  xpsmet  24268  tmsxms  24372  tmsms  24373  imasf1oxms  24375  imasf1oms  24376  prdsxms  24416  prdsms  24417  tmsxpsval  24424  retopbas  24646  cnngp  24665  cnopn  24672  cnperf  24707  retopconn  24716  fsumcn  24759  abscncf  24792  recncf  24793  imcncf  24794  cjcncf  24795  mulc1cncf  24796  cncfcn1  24802  cncfmpt2f  24806  cncfmpt2ss  24807  addccncf  24808  idcncf  24809  sub1cncf  24810  sub2cncf  24811  cdivcncf  24812  negcncf  24813  negcncfOLD  24814  negfcncf  24815  abscncfALT  24816  cnmpopc  24820  xrhmeo  24842  oprpiece1res1  24847  oprpiece1res2  24848  cnrehmeo  24849  cnrehmeoOLD  24850  iscau3  25176  caubl  25206  caublcls  25207  mulcncf  25344  evthicc2  25359  ovolre  25424  volsuplem  25454  uniiccdif  25477  uniioovol  25478  uniiccvol  25479  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  dyadmbllem  25498  volivth  25506  itgfsum  25726  iblabslem  25727  iblabs  25728  bddmulibl  25738  cnlimc  25787  cnlimci  25788  dvcnp2  25819  dvcnp2OLD  25820  dvcn  25821  cpnord  25835  cpnres  25837  dvmptntr  25873  dvmptfsum  25877  rolle  25892  dvlipcn  25897  c1liplem1  25899  dvivth  25913  dvfsumabs  25927  ftc1a  25942  ftc1cn  25948  plyssc  26103  plyeq0  26114  0dgr  26148  coemulc  26158  coe0  26159  coesub  26160  coe1termlem  26161  dgrmulc  26175  dgrsub  26176  dvnply2  26193  plycpn  26195  plyremlem  26210  fta1lem  26213  vieta1lem2  26217  aalioulem3  26240  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmcn  26306  psercn  26334  abelth  26349  efcn  26351  efcvx  26357  dvrelog  26544  logcn  26554  dvloglem  26555  dvlog  26558  dvlog2  26560  efopnlem2  26564  logccv  26570  cxpcn  26652  cxpcnOLD  26653  cxpcn3  26656  resqrtcn  26657  sqrtcn  26658  loglesqrt  26669  atancn  26844  jensen  26897  ftalem3  26983  dchrfi  27164  dchrisumlema  27397  pntlem3  27518  madebday  27814  expscl  28323  uhgrsubgrself  29225  uhgrspansubgr  29236  umgr2adedgwlk  29890  umgr2adedgwlkon  29891  umgr2adedgspth  29893  upgr1wlkdlem2  30090  sspid  30669  ssps  30674  helch  31187  hhssnv  31208  hhsssh  31213  shintcl  31274  chintcl  31276  shlesb1i  31330  omlsi  31348  chlejb1i  31420  chm0i  31434  chabs1  31460  chabs2  31461  spanun  31489  cmidi  31554  pjidmcoi  32121  csmdsymi  32278  sumdmdlem2  32363  dmdbr5ati  32366  mdcompli  32373  dmdcompli  32374  disjdifprg  32519  fcoinver  32548  f1rnen  32571  xppreima  32588  padct  32662  xrinfm  32698  clatp0cl  32918  clatp1cl  32919  xrsp0  32966  xrsp1  32967  cntrcrng  33023  cycpmconjslem1  33096  cycpmconjslem2  33097  gsumvsca1  33168  gsumvsca2  33169  qusxpid  33300  ellspds  33305  rspidlid  33312  rlmdim  33576  reff  33806  locfinreflem  33807  esumsnf  34031  esumcvg  34053  sigagenid  34118  iblidicc  34560  cxpcncf1  34563  fdvposlt  34567  fdvneggt  34568  fdvposle  34569  fdvnegge  34570  logdivsqrle  34618  bnj1253  34984  fineqvac  35072  fineqvnttrclse  35077  cvmlift2lem6  35285  satfun  35388  mrsubrn  35490  elmrsubrn  35497  elmsubrn  35505  msubrn  35506  imagesset  35931  ivthALT  36313  fness  36327  fneref  36328  refssfne  36336  fnemeet1  36344  fnejoin2  36347  filnetlem2  36357  filnetlem4  36359  ontgval  36409  knoppcnlem10  36480  knoppcnlem11  36481  bj-rabtr  36908  bj-rabtrAUTO  36910  bj-disj2r  37006  bj-restsnid  37065  bj-resta  37074  bj-imdirco  37168  elxp8  37349  finorwe  37360  mblfinlem3  37643  mblfinlem4  37644  ismblfin  37645  ovoliunnfl  37646  voliunnfl  37648  volsupnfl  37649  mbfposadd  37651  ftc1cnnclem  37675  ftc1cnnc  37676  ftc1anc  37685  ftc2nc  37686  areacirclem2  37693  areacirclem4  37695  areacirc  37697  caures  37744  constcncf  37746  brssrid  38483  brcnvssrid  38488  refrelid  38503  n0eldmqs  38629  atpsubN  39736  pol1N  39893  dia2dimlem13  41059  dibord  41142  dochvalr  41340  hdmapevec  41818  lcmineqlem10  42015  lcmineqlem12  42017  ismrcd1  42675  ismrc  42678  incssnn0  42688  mzpclall  42704  rmydioph  42991  rmxdioph  42993  expdiophlem2  42999  expdioph  43000  aomclem6  43036  kelac1  43040  gicabl  43076  arearect  43192  areaquad  43193  unielid  43196  oege2  43284  oacl2g  43307  ofoaf  43332  clcnvlem  43600  cnvtrcl0  43603  fvilbd  43666  relexp0a  43693  corcltrcl  43716  clsk1indlem2  44019  ntrclskb  44046  wnefimgd  44138  mnuprdlem4  44252  nzss  44294  lhe4.4ex1a  44306  dvsconst  44307  dvsid  44308  dvsef  44309  binomcxplemnn0  44326  onfrALTlem3  44522  onfrALTlem3VD  44864  unisn0  45036  founiiun0  45172  evthiccabs  45481  climconstmpt  45643  cncfshift  45859  addccncf2  45861  cncfcompt  45868  ioccncflimc  45870  icocncflimc  45874  cncfiooicclem1  45878  cncfiooicc  45879  cncfiooiccre  45880  cxpcncf2  45884  add1cncf  45886  add2cncf  45887  sub1cncfd  45888  sub2cncfd  45889  dvcosre  45897  dvmptfprod  45930  ibliooicc  45956  itgsincmulx  45959  itgsubsticclem  45960  itgiccshift  45965  itgperiod  45966  itgsbtaddcnst  45967  dirkeritg  46087  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem16  46108  fourierdlem18  46110  fourierdlem21  46113  fourierdlem22  46114  fourierdlem23  46115  fourierdlem32  46124  fourierdlem33  46125  fourierdlem39  46131  fourierdlem40  46132  fourierdlem57  46148  fourierdlem58  46149  fourierdlem59  46150  fourierdlem62  46153  fourierdlem68  46159  fourierdlem72  46163  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem78  46169  fourierdlem83  46174  fourierdlem84  46175  fourierdlem85  46176  fourierdlem88  46179  fourierdlem93  46184  fourierdlem94  46185  fourierdlem95  46186  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  fourierdlem112  46203  fourierdlem113  46204  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  fouriercn  46217  etransclem18  46237  etransclem22  46241  etransclem34  46253  etransclem46  46265  etransclem47  46266  sge0fsum  46372  meaiininclem  46471  hoidmvlelem2  46581  hspdifhsp  46601  hspmbllem2  46612  hspmbl  46614  iinhoiicclem  46658  pimgtmnf2  46699  smflimsuplem1  46805  smflimsuplem6  46810  cjnpoly  46877  srhmsubcALTV  48313  imaidfu2lem  49098  imaidfu  49099  imaidfu2  49100  setc1onsubc  49591