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 2114   ⊆ wss 3903

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

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  4222  difidALT  4331  inv1  4352  disjpss  4415  pwidg  4576  elssuni  4896  unimax  4902  intmin  4925  rintn0  5066  sseliALT  5256  inxpssres  5649  xpss1  5651  xpss2  5652  residm  5977  resdm  5993  resmpt3  6005  cnvrescnv  6161  onelssex  6374  ordunidif  6375  funresfunco  6541  dffn3  6682  fdmrn  6701  fvreseq1  6993  iunpw  7726  onsucuni  7780  tfisi  7811  fparlem3  8066  fparlem4  8067  funsssuppss  8142  tfrlem1  8317  tz7.48-2  8383  oaordi  8483  omwordi  8508  omass  8517  nnaordi  8556  nnmwordi  8573  naddunif  8631  fpmg  8818  boxcutc  8891  domss2  9076  findcard2d  9103  fimax2g  9198  domunfican  9234  fipreima  9270  fimin2g  9414  wofib  9462  wemapso  9468  noinfep  9581  cantnfval2  9590  tcidm  9665  tc0  9666  r1rankidb  9728  r1pw  9769  rankr1id  9786  scott0  9810  xpomen  9937  infpwfien  9984  alephsmo  10024  dfac12lem3  10068  cflem  10167  cflemOLD  10168  cflecard  10175  cfslb  10188  fin4en1  10231  fin23lem13  10254  fin23lem36  10270  isf32lem1  10275  fin67  10317  dcomex  10369  zorn2lem4  10421  alephexp2  10504  fpwwe2lem12  10565  canthnumlem  10571  wuncidm  10669  eltsk2g  10674  axgroth6  10751  axgroth3  10754  xrsup  13800  expcl  14014  hashcard  14290  hashf1lem2  14391  xptrrel  14915  cotrtrclfv  14947  rtrclreclem2  14994  lo1eq  15503  rlimeq  15504  serclim0  15512  isercolllem2  15601  isercoll  15603  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  fprod2d  15916  risefaccl  15950  fallfaccl  15951  eflt  16054  rpnnen2lem3  16153  rpnnen2lem5  16155  rpnnen2lem12  16162  rexpen  16165  ressbasssg  17176  ressid  17183  ressinbas  17184  oduclatb  18442  ipopos  18471  fpwipodrs  18475  ghmghmrn  19176  elcntr  19271  cntrnsg  19285  0symgefmndeq  19335  sylow3lem5  19572  lsmss1  19606  lsmss2  19608  cmnbascntr  19746  cntrcmnd  19783  cntrabl  19784  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumadd  19864  gsumzmhm  19878  gsumzoppg  19885  dprdf1  19976  ablfac1eulem  20015  gsumle  20086  subrgid  20518  srhmsubc  20625  lbsextlem1  21125  rlmval2  21156  znf1o  21518  zntoslem  21523  css0  21656  uvcresum  21760  frlmlbs  21764  psrass1lem  21900  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  mdetunilem9  22576  smadiadetglem1  22627  smadiadetglem2  22628  pmatcollpw3  22740  topopn  22862  fiinbas  22908  topbas  22928  topcld  22991  ntrtop  23026  opnneissb  23070  opnssneib  23071  opnneiid  23082  maxlp  23103  isperf2  23108  restperf  23140  idcn  23213  cnconst2  23239  lmres  23256  fiuncmp  23360  1stcelcls  23417  ssref  23468  refref  23469  kgencn2  23513  ptpjpre1  23527  ptbasfi  23537  xkopt  23611  elqtop2  23657  ptcmpfi  23769  fbssfi  23793  opnfbas  23798  filtop  23811  isfil2  23812  isfild  23814  fsubbas  23823  ssfg  23828  filssufilg  23867  ufileu  23875  imaelfm  23907  rnelfm  23909  fmfnfmlem4  23913  neiflim  23930  fclscf  23981  flimfnfcls  23984  tsmsfbas  24084  xpsxmet  24336  xpsdsval  24337  xpsmet  24338  tmsxms  24442  tmsms  24443  imasf1oxms  24445  imasf1oms  24446  prdsxms  24486  prdsms  24487  tmsxpsval  24494  retopbas  24716  cnngp  24735  cnopn  24742  cnperf  24777  retopconn  24786  fsumcn  24829  abscncf  24862  recncf  24863  imcncf  24864  cjcncf  24865  mulc1cncf  24866  cncfcn1  24872  cncfmpt2f  24876  cncfmpt2ss  24877  addccncf  24878  idcncf  24879  sub1cncf  24880  sub2cncf  24881  cdivcncf  24882  negcncf  24883  negcncfOLD  24884  negfcncf  24885  abscncfALT  24886  cnmpopc  24890  xrhmeo  24912  oprpiece1res1  24917  oprpiece1res2  24918  cnrehmeo  24919  cnrehmeoOLD  24920  iscau3  25246  caubl  25276  caublcls  25277  mulcncf  25414  evthicc2  25429  ovolre  25494  volsuplem  25524  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  dyadmbllem  25568  volivth  25576  itgfsum  25796  iblabslem  25797  iblabs  25798  bddmulibl  25808  cnlimc  25857  cnlimci  25858  dvcnp2  25889  dvcnp2OLD  25890  dvcn  25891  cpnord  25905  cpnres  25907  dvmptntr  25943  dvmptfsum  25947  rolle  25962  dvlipcn  25967  c1liplem1  25969  dvivth  25983  dvfsumabs  25997  ftc1a  26012  ftc1cn  26018  plyssc  26173  plyeq0  26184  0dgr  26218  coemulc  26228  coe0  26229  coesub  26230  coe1termlem  26231  dgrmulc  26245  dgrsub  26246  dvnply2  26263  plycpn  26265  plyremlem  26280  fta1lem  26283  vieta1lem2  26287  aalioulem3  26310  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmcn  26376  psercn  26404  abelth  26419  efcn  26421  efcvx  26427  dvrelog  26614  logcn  26624  dvloglem  26625  dvlog  26628  dvlog2  26630  efopnlem2  26634  logccv  26640  cxpcn  26722  cxpcnOLD  26723  cxpcn3  26726  resqrtcn  26727  sqrtcn  26728  loglesqrt  26739  atancn  26914  jensen  26967  ftalem3  27053  dchrfi  27234  dchrisumlema  27467  pntlem3  27588  madebday  27908  expscl  28439  bdaypw2n0bndlem  28471  uhgrsubgrself  29365  uhgrspansubgr  29376  umgr2adedgwlk  30030  umgr2adedgwlkon  30031  umgr2adedgspth  30033  upgr1wlkdlem2  30233  sspid  30812  ssps  30817  helch  31330  hhssnv  31351  hhsssh  31356  shintcl  31417  chintcl  31419  shlesb1i  31473  omlsi  31491  chlejb1i  31563  chm0i  31577  chabs1  31603  chabs2  31604  spanun  31632  cmidi  31697  pjidmcoi  32264  csmdsymi  32421  sumdmdlem2  32506  dmdbr5ati  32509  mdcompli  32516  dmdcompli  32517  disjdifprg  32661  fcoinver  32690  f1rnen  32717  xppreima  32734  padct  32807  xrinfm  32845  indconst1  32950  clatp0cl  33068  clatp1cl  33069  xrsp0  33104  xrsp1  33105  cntrcrng  33174  cycpmconjslem1  33247  cycpmconjslem2  33248  gsumvsca1  33319  gsumvsca2  33320  qusxpid  33455  ellspds  33460  rspidlid  33467  rlmdim  33786  reff  34016  locfinreflem  34017  esumsnf  34241  esumcvg  34263  sigagenid  34328  iblidicc  34769  cxpcncf1  34772  fdvposlt  34776  fdvneggt  34777  fdvposle  34778  fdvnegge  34779  logdivsqrle  34827  bnj1253  35192  fineqvac  35291  fineqvnttrclse  35299  noinfepfnregs  35307  cvmlift2lem6  35521  satfun  35624  mrsubrn  35726  elmrsubrn  35733  elmsubrn  35741  msubrn  35742  imagesset  36166  ivthALT  36548  fness  36562  fneref  36563  refssfne  36571  fnemeet1  36579  fnejoin2  36582  filnetlem2  36592  filnetlem4  36594  ontgval  36644  knoppcnlem10  36721  knoppcnlem11  36722  bj-rabtr  37172  bj-rabtrAUTO  37174  bj-disj2r  37270  bj-restsnid  37334  bj-resta  37343  bj-imdirco  37439  elxp8  37620  finorwe  37631  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  mbfposadd  37912  ftc1cnnclem  37936  ftc1cnnc  37937  ftc1anc  37946  ftc2nc  37947  areacirclem2  37954  areacirclem4  37956  areacirc  37958  caures  38005  constcncf  38007  brssrid  38827  brcnvssrid  38832  refrelid  38847  n0eldmqs  38977  atpsubN  40123  pol1N  40280  dia2dimlem13  41446  dibord  41529  dochvalr  41727  hdmapevec  42205  lcmineqlem10  42402  lcmineqlem12  42404  ismrcd1  43049  ismrc  43052  incssnn0  43062  mzpclall  43078  rmydioph  43365  rmxdioph  43367  expdiophlem2  43373  expdioph  43374  aomclem6  43410  kelac1  43414  gicabl  43450  arearect  43566  areaquad  43567  unielid  43570  oege2  43658  oacl2g  43681  ofoaf  43706  clcnvlem  43973  cnvtrcl0  43976  fvilbd  44039  relexp0a  44066  corcltrcl  44089  clsk1indlem2  44392  ntrclskb  44419  wnefimgd  44511  mnuprdlem4  44625  nzss  44667  lhe4.4ex1a  44679  dvsconst  44680  dvsid  44681  dvsef  44682  binomcxplemnn0  44699  onfrALTlem3  44894  onfrALTlem3VD  45236  unisn0  45408  founiiun0  45543  evthiccabs  45850  climconstmpt  46010  cncfshift  46226  addccncf2  46228  cncfcompt  46235  ioccncflimc  46237  icocncflimc  46241  cncfiooicclem1  46245  cncfiooicc  46246  cncfiooiccre  46247  cxpcncf2  46251  add1cncf  46253  add2cncf  46254  sub1cncfd  46255  sub2cncfd  46256  dvcosre  46264  dvmptfprod  46297  ibliooicc  46323  itgsincmulx  46326  itgsubsticclem  46327  itgiccshift  46332  itgperiod  46333  itgsbtaddcnst  46334  dirkeritg  46454  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem16  46475  fourierdlem18  46477  fourierdlem21  46480  fourierdlem22  46481  fourierdlem23  46482  fourierdlem32  46491  fourierdlem33  46492  fourierdlem39  46498  fourierdlem40  46499  fourierdlem57  46515  fourierdlem58  46516  fourierdlem59  46517  fourierdlem62  46520  fourierdlem68  46526  fourierdlem72  46530  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem78  46536  fourierdlem83  46541  fourierdlem84  46542  fourierdlem85  46543  fourierdlem88  46546  fourierdlem93  46551  fourierdlem94  46552  fourierdlem95  46553  fourierdlem97  46555  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem112  46570  fourierdlem113  46571  sqwvfoura  46580  sqwvfourb  46581  fouriersw  46583  fouriercn  46584  etransclem18  46604  etransclem22  46608  etransclem34  46620  etransclem46  46632  etransclem47  46633  sge0fsum  46739  meaiininclem  46838  hoidmvlelem2  46948  hspdifhsp  46968  hspmbllem2  46979  hspmbl  46981  iinhoiicclem  47025  pimgtmnf2  47066  smflimsuplem1  47172  smflimsuplem6  47177  cjnpoly  47243  srhmsubcALTV  48679  imaidfu2lem  49462  imaidfu  49463  imaidfu2  49464  setc1onsubc  49955