Theorem ssid 3957

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

Syntax hints:   ∈ wcel 2111   ⊆ wss 3902

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

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

This theorem is referenced by:  ssidd  3958  eqimssd  3991  eqimsscd  3992  eqimssi  3995  eqimss2i  3996  nsspssun  4218  difidALT  4327  inv1  4348  disjpss  4411  pwidg  4570  elssuni  4889  unimax  4895  intmin  4918  rintn0  5057  sseliALT  5247  inxpssres  5633  xpss1  5635  xpss2  5636  residm  5959  resdm  5975  resmpt3  5987  cnvrescnv  6142  onelssex  6355  ordunidif  6356  funresfunco  6522  dffn3  6663  fdmrn  6682  fvreseq1  6972  iunpw  7704  onsucuni  7758  tfisi  7789  fparlem3  8044  fparlem4  8045  funsssuppss  8120  tfrlem1  8295  tz7.48-2  8361  oaordi  8461  omwordi  8486  omass  8495  nnaordi  8533  nnmwordi  8550  naddunif  8608  fpmg  8792  boxcutc  8865  domss2  9049  findcard2d  9076  fimax2g  9170  domunfican  9206  fipreima  9242  fimin2g  9383  wofib  9431  wemapso  9437  noinfep  9550  cantnfval2  9559  tcidm  9636  tc0  9637  r1rankidb  9694  r1pw  9735  rankr1id  9752  scott0  9776  xpomen  9903  infpwfien  9950  alephsmo  9990  dfac12lem3  10034  cflem  10133  cflemOLD  10134  cflecard  10141  cfslb  10154  fin4en1  10197  fin23lem13  10220  fin23lem36  10236  isf32lem1  10241  fin67  10283  dcomex  10335  zorn2lem4  10387  alephexp2  10469  fpwwe2lem12  10530  canthnumlem  10536  wuncidm  10634  eltsk2g  10639  axgroth6  10716  axgroth3  10719  xrsup  13769  expcl  13983  hashcard  14259  hashf1lem2  14360  xptrrel  14884  cotrtrclfv  14916  rtrclreclem2  14963  lo1eq  15472  rlimeq  15473  serclim0  15481  isercolllem2  15570  isercoll  15572  fsum2d  15675  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  fprod2d  15885  risefaccl  15919  fallfaccl  15920  eflt  16023  rpnnen2lem3  16122  rpnnen2lem5  16124  rpnnen2lem12  16131  rexpen  16134  ressbasssg  17145  ressid  17152  ressinbas  17153  oduclatb  18410  ipopos  18439  fpwipodrs  18443  ghmghmrn  19145  elcntr  19240  cntrnsg  19254  0symgefmndeq  19304  sylow3lem5  19541  lsmss1  19575  lsmss2  19577  cmnbascntr  19715  cntrcmnd  19752  cntrabl  19753  gsumzres  19819  gsumzcl2  19820  gsumzf1o  19822  gsumadd  19833  gsumzmhm  19847  gsumzoppg  19854  dprdf1  19945  ablfac1eulem  19984  gsumle  20055  subrgid  20486  srhmsubc  20593  lbsextlem1  21093  rlmval2  21124  znf1o  21486  zntoslem  21491  css0  21624  uvcresum  21728  frlmlbs  21732  psrass1lem  21867  mdetrsca2  22517  mdetrlin2  22520  mdetunilem5  22529  mdetunilem9  22533  smadiadetglem1  22584  smadiadetglem2  22585  pmatcollpw3  22697  topopn  22819  fiinbas  22865  topbas  22885  topcld  22948  ntrtop  22983  opnneissb  23027  opnssneib  23028  opnneiid  23039  maxlp  23060  isperf2  23065  restperf  23097  idcn  23170  cnconst2  23196  lmres  23213  fiuncmp  23317  1stcelcls  23374  ssref  23425  refref  23426  kgencn2  23470  ptpjpre1  23484  ptbasfi  23494  xkopt  23568  elqtop2  23614  ptcmpfi  23726  fbssfi  23750  opnfbas  23755  filtop  23768  isfil2  23769  isfild  23771  fsubbas  23780  ssfg  23785  filssufilg  23824  ufileu  23832  imaelfm  23864  rnelfm  23866  fmfnfmlem4  23870  neiflim  23887  fclscf  23938  flimfnfcls  23941  tsmsfbas  24041  xpsxmet  24293  xpsdsval  24294  xpsmet  24295  tmsxms  24399  tmsms  24400  imasf1oxms  24402  imasf1oms  24403  prdsxms  24443  prdsms  24444  tmsxpsval  24451  retopbas  24673  cnngp  24692  cnopn  24699  cnperf  24734  retopconn  24743  fsumcn  24786  abscncf  24819  recncf  24820  imcncf  24821  cjcncf  24822  mulc1cncf  24823  cncfcn1  24829  cncfmpt2f  24833  cncfmpt2ss  24834  addccncf  24835  idcncf  24836  sub1cncf  24837  sub2cncf  24838  cdivcncf  24839  negcncf  24840  negcncfOLD  24841  negfcncf  24842  abscncfALT  24843  cnmpopc  24847  xrhmeo  24869  oprpiece1res1  24874  oprpiece1res2  24875  cnrehmeo  24876  cnrehmeoOLD  24877  iscau3  25203  caubl  25233  caublcls  25234  mulcncf  25371  evthicc2  25386  ovolre  25451  volsuplem  25481  uniiccdif  25504  uniioovol  25505  uniiccvol  25506  uniioombllem3  25511  uniioombllem4  25512  uniioombllem5  25513  dyadmbllem  25525  volivth  25533  itgfsum  25753  iblabslem  25754  iblabs  25755  bddmulibl  25765  cnlimc  25814  cnlimci  25815  dvcnp2  25846  dvcnp2OLD  25847  dvcn  25848  cpnord  25862  cpnres  25864  dvmptntr  25900  dvmptfsum  25904  rolle  25919  dvlipcn  25924  c1liplem1  25926  dvivth  25940  dvfsumabs  25954  ftc1a  25969  ftc1cn  25975  plyssc  26130  plyeq0  26141  0dgr  26175  coemulc  26185  coe0  26186  coesub  26187  coe1termlem  26188  dgrmulc  26202  dgrsub  26203  dvnply2  26220  plycpn  26222  plyremlem  26237  fta1lem  26240  vieta1lem2  26244  aalioulem3  26267  taylthlem1  26306  taylthlem2  26307  taylthlem2OLD  26308  ulmcn  26333  psercn  26361  abelth  26376  efcn  26378  efcvx  26384  dvrelog  26571  logcn  26581  dvloglem  26582  dvlog  26585  dvlog2  26587  efopnlem2  26591  logccv  26597  cxpcn  26679  cxpcnOLD  26680  cxpcn3  26683  resqrtcn  26684  sqrtcn  26685  loglesqrt  26696  atancn  26871  jensen  26924  ftalem3  27010  dchrfi  27191  dchrisumlema  27424  pntlem3  27545  madebday  27843  expscl  28352  uhgrsubgrself  29256  uhgrspansubgr  29267  umgr2adedgwlk  29921  umgr2adedgwlkon  29922  umgr2adedgspth  29924  upgr1wlkdlem2  30121  sspid  30700  ssps  30705  helch  31218  hhssnv  31239  hhsssh  31244  shintcl  31305  chintcl  31307  shlesb1i  31361  omlsi  31379  chlejb1i  31451  chm0i  31465  chabs1  31491  chabs2  31492  spanun  31520  cmidi  31585  pjidmcoi  32152  csmdsymi  32309  sumdmdlem2  32394  dmdbr5ati  32397  mdcompli  32404  dmdcompli  32405  disjdifprg  32550  fcoinver  32579  f1rnen  32605  xppreima  32622  padct  32696  xrinfm  32733  clatp0cl  32952  clatp1cl  32953  xrsp0  32988  xrsp1  32989  cntrcrng  33045  cycpmconjslem1  33118  cycpmconjslem2  33119  gsumvsca1  33190  gsumvsca2  33191  qusxpid  33323  ellspds  33328  rspidlid  33335  rlmdim  33617  reff  33847  locfinreflem  33848  esumsnf  34072  esumcvg  34094  sigagenid  34159  iblidicc  34600  cxpcncf1  34603  fdvposlt  34607  fdvneggt  34608  fdvposle  34609  fdvnegge  34610  logdivsqrle  34658  bnj1253  35024  fineqvac  35127  fineqvnttrclse  35132  cvmlift2lem6  35340  satfun  35443  mrsubrn  35545  elmrsubrn  35552  elmsubrn  35560  msubrn  35561  imagesset  35986  ivthALT  36368  fness  36382  fneref  36383  refssfne  36391  fnemeet1  36399  fnejoin2  36402  filnetlem2  36412  filnetlem4  36414  ontgval  36464  knoppcnlem10  36535  knoppcnlem11  36536  bj-rabtr  36963  bj-rabtrAUTO  36965  bj-disj2r  37061  bj-restsnid  37120  bj-resta  37129  bj-imdirco  37223  elxp8  37404  finorwe  37415  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  mbfposadd  37706  ftc1cnnclem  37730  ftc1cnnc  37731  ftc1anc  37740  ftc2nc  37741  areacirclem2  37748  areacirclem4  37750  areacirc  37752  caures  37799  constcncf  37801  brssrid  38538  brcnvssrid  38543  refrelid  38558  n0eldmqs  38684  atpsubN  39791  pol1N  39948  dia2dimlem13  41114  dibord  41197  dochvalr  41395  hdmapevec  41873  lcmineqlem10  42070  lcmineqlem12  42072  ismrcd1  42730  ismrc  42733  incssnn0  42743  mzpclall  42759  rmydioph  43046  rmxdioph  43048  expdiophlem2  43054  expdioph  43055  aomclem6  43091  kelac1  43095  gicabl  43131  arearect  43247  areaquad  43248  unielid  43251  oege2  43339  oacl2g  43362  ofoaf  43387  clcnvlem  43655  cnvtrcl0  43658  fvilbd  43721  relexp0a  43748  corcltrcl  43771  clsk1indlem2  44074  ntrclskb  44101  wnefimgd  44193  mnuprdlem4  44307  nzss  44349  lhe4.4ex1a  44361  dvsconst  44362  dvsid  44363  dvsef  44364  binomcxplemnn0  44381  onfrALTlem3  44576  onfrALTlem3VD  44918  unisn0  45090  founiiun0  45226  evthiccabs  45535  climconstmpt  45695  cncfshift  45911  addccncf2  45913  cncfcompt  45920  ioccncflimc  45922  icocncflimc  45926  cncfiooicclem1  45930  cncfiooicc  45931  cncfiooiccre  45932  cxpcncf2  45936  add1cncf  45938  add2cncf  45939  sub1cncfd  45940  sub2cncfd  45941  dvcosre  45949  dvmptfprod  45982  ibliooicc  46008  itgsincmulx  46011  itgsubsticclem  46012  itgiccshift  46017  itgperiod  46018  itgsbtaddcnst  46019  dirkeritg  46139  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem16  46160  fourierdlem18  46162  fourierdlem21  46165  fourierdlem22  46166  fourierdlem23  46167  fourierdlem32  46176  fourierdlem33  46177  fourierdlem39  46183  fourierdlem40  46184  fourierdlem57  46200  fourierdlem58  46201  fourierdlem59  46202  fourierdlem62  46205  fourierdlem68  46211  fourierdlem72  46215  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem78  46221  fourierdlem83  46226  fourierdlem84  46227  fourierdlem85  46228  fourierdlem88  46231  fourierdlem93  46236  fourierdlem94  46237  fourierdlem95  46238  fourierdlem97  46240  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  fourierdlem113  46256  sqwvfoura  46265  sqwvfourb  46266  fouriersw  46268  fouriercn  46269  etransclem18  46289  etransclem22  46293  etransclem34  46305  etransclem46  46317  etransclem47  46318  sge0fsum  46424  meaiininclem  46523  hoidmvlelem2  46633  hspdifhsp  46653  hspmbllem2  46664  hspmbl  46666  iinhoiicclem  46710  pimgtmnf2  46751  smflimsuplem1  46857  smflimsuplem6  46862  cjnpoly  46919  srhmsubcALTV  48355  imaidfu2lem  49140  imaidfu  49141  imaidfu2  49142  setc1onsubc  49633