Theorem ssid 3945

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

Syntax hints:   ∈ wcel 2101   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-in 3896  df-ss 3906

This theorem is referenced by:  ssidd  3946  eqimssi  3981  eqimss2i  3982  nsspssun  4194  difidALT  4308  inv1  4331  disjpss  4397  pwidg  4558  elssuni  4874  unimax  4880  intmin  4902  rintn0  5041  sseliALT  5236  inxpssres  5608  xpss1  5610  xpss2  5611  residm  5927  resdm  5939  resmpt3  5949  cnvrescnv  6102  ordunidif  6318  funresfunco  6492  dffn3  6631  fdmrn  6650  fvreseq1  6936  fimacnvOLD  6968  iunpw  7641  onsucuni  7695  tfisi  7725  fparlem3  7974  fparlem4  7975  funsssuppss  8026  tfrlem1  8227  tz7.48-2  8293  oaordi  8397  omwordi  8422  omass  8431  nnaordi  8469  nnmwordi  8486  fpmg  8676  boxcutc  8749  domss2  8948  findcard2d  8974  0fin  8979  en1eqsn  9076  fimax2g  9088  domunfican  9115  pwfiOLD  9142  fipreima  9153  fimin2g  9284  wofib  9332  wemapso  9338  noinfep  9446  cantnfval2  9455  tcidm  9532  tc0  9533  r1rankidb  9590  r1pw  9631  rankr1id  9648  scott0  9672  xpomen  9799  infpwfien  9846  alephsmo  9886  dfac12lem3  9929  cflem  10030  cflecard  10037  cfslb  10050  fin4en1  10093  fin23lem13  10116  fin23lem36  10132  isf32lem1  10137  fin67  10179  dcomex  10231  zorn2lem4  10283  alephexp2  10365  fpwwe2lem12  10426  canthnumlem  10432  wuncidm  10530  eltsk2g  10535  axgroth6  10612  axgroth3  10615  xrsup  13616  expcl  13828  hashcard  14098  hashf1lem2  14198  xptrrel  14719  cotrtrclfv  14751  rtrclreclem2  14798  lo1eq  15305  rlimeq  15306  serclim0  15314  isercolllem2  15405  isercoll  15407  fsum2d  15511  fsumabs  15541  fsumrlim  15551  fsumo1  15552  fsumiun  15561  fprod2d  15719  risefaccl  15753  fallfaccl  15754  eflt  15854  rpnnen2lem3  15953  rpnnen2lem5  15955  rpnnen2lem12  15962  rexpen  15965  ressid  16982  ressinbas  16983  oduclatb  18253  ipopos  18282  fpwipodrs  18286  ghmghmrn  18881  cntrnsg  18976  0symgefmndeq  19029  sylow3lem5  19264  lsmss1  19299  lsmss2  19301  cntrcmnd  19471  cntrabl  19472  gsumzres  19538  gsumzcl2  19539  gsumzf1o  19541  gsumadd  19552  gsumzmhm  19566  gsumzoppg  19573  dprdf1  19664  ablfac1eulem  19703  subrgid  20054  lbsextlem1  20448  rlmval2  20492  znf1o  20787  zntoslem  20792  css0  20922  uvcresum  21028  frlmlbs  21032  psrass1lemOLD  21171  psrass1lem  21174  mdetrsca2  21781  mdetrlin2  21784  mdetunilem5  21793  mdetunilem9  21797  smadiadetglem1  21848  smadiadetglem2  21849  pmatcollpw3  21961  topopn  22083  fiinbas  22130  topbas  22150  topcld  22214  ntrtop  22249  opnneissb  22293  opnssneib  22294  opnneiid  22305  maxlp  22326  isperf2  22331  restperf  22363  idcn  22436  cnconst2  22462  lmres  22479  fiuncmp  22583  1stcelcls  22640  ssref  22691  refref  22692  kgencn2  22736  ptpjpre1  22750  ptbasfi  22760  xkopt  22834  elqtop2  22880  ptcmpfi  22992  fbssfi  23016  opnfbas  23021  filtop  23034  isfil2  23035  isfild  23037  fsubbas  23046  ssfg  23051  filssufilg  23090  ufileu  23098  imaelfm  23130  rnelfm  23132  fmfnfmlem4  23136  neiflim  23153  fclscf  23204  flimfnfcls  23207  tsmsfbas  23307  xpsxmet  23561  xpsdsval  23562  xpsmet  23563  tmsxms  23670  tmsms  23671  imasf1oxms  23673  imasf1oms  23674  prdsxms  23714  prdsms  23715  tmsxpsval  23722  retopbas  23952  cnngp  23971  cnopn  23978  cnperf  24011  retopconn  24020  fsumcn  24061  abscncf  24092  recncf  24093  imcncf  24094  cjcncf  24095  mulc1cncf  24096  cncfcn1  24102  cncfmpt2f  24106  cncfmpt2ss  24107  addccncf  24108  idcncf  24109  sub1cncf  24110  sub2cncf  24111  cdivcncf  24112  negcncf  24113  negfcncf  24114  abscncfALT  24115  cnmpopc  24119  xrhmeo  24137  oprpiece1res1  24142  oprpiece1res2  24143  cnrehmeo  24144  iscau3  24470  caubl  24500  caublcls  24501  evthicc2  24652  ovolre  24717  volsuplem  24747  uniiccdif  24770  uniioovol  24771  uniiccvol  24772  uniioombllem3  24777  uniioombllem4  24778  uniioombllem5  24779  dyadmbllem  24791  volivth  24799  itgfsum  25019  iblabslem  25020  iblabs  25021  bddmulibl  25031  cnlimc  25080  cnlimci  25081  dvcnp2  25112  dvcn  25113  cpnord  25127  cpnres  25129  dvmptntr  25163  dvmptfsum  25167  rolle  25182  dvlipcn  25186  c1liplem1  25188  dvivth  25202  dvfsumabs  25215  ftc1a  25229  ftc1cn  25235  plyssc  25389  plyeq0  25400  0dgr  25434  coemulc  25444  coe0  25445  coesub  25446  coe1termlem  25447  dgrmulc  25460  dgrsub  25461  dvnply2  25475  plycpn  25477  plyremlem  25492  fta1lem  25495  vieta1lem2  25499  aalioulem3  25522  taylthlem1  25560  taylthlem2  25561  ulmcn  25586  psercn  25613  abelth  25628  efcn  25630  efcvx  25636  dvrelog  25820  logcn  25830  dvloglem  25831  dvlog  25834  dvlog2  25836  efopnlem2  25840  logccv  25846  cxpcn  25926  cxpcn3  25929  resqrtcn  25930  sqrtcn  25931  loglesqrt  25939  atancn  26114  jensen  26166  ftalem3  26252  dchrfi  26431  dchrisumlema  26664  pntlem3  26785  uhgrsubgrself  27675  uhgrspansubgr  27686  umgr2adedgwlk  28338  umgr2adedgwlkon  28339  umgr2adedgspth  28341  upgr1wlkdlem2  28538  sspid  29115  ssps  29120  helch  29633  hhssnv  29654  hhsssh  29659  shintcl  29720  chintcl  29722  shlesb1i  29776  omlsi  29794  chlejb1i  29866  chm0i  29880  chabs1  29906  chabs2  29907  spanun  29935  cmidi  30000  pjidmcoi  30567  csmdsymi  30724  sumdmdlem2  30809  dmdbr5ati  30812  mdcompli  30819  dmdcompli  30820  disjdifprg  30942  fcoinver  30974  f1rnen  30992  xppreima  31011  padct  31082  xrinfm  31105  clatp0cl  31282  clatp1cl  31283  xrsp0  31318  xrsp1  31319  cntrcrng  31350  gsumle  31378  cycpmconjslem1  31449  cycpmconjslem2  31450  gsumvsca1  31507  gsumvsca2  31508  qusxpid  31587  ellspds  31592  rspidlid  31598  reff  31817  locfinreflem  31818  esumsnf  32060  esumcvg  32082  sigagenid  32147  iblidicc  32600  cxpcncf1  32603  fdvposlt  32607  fdvneggt  32608  fdvposle  32609  fdvnegge  32610  logdivsqrle  32658  bnj1253  33025  fineqvac  33094  cvmlift2lem6  33298  satfun  33401  mrsubrn  33503  elmrsubrn  33510  elmsubrn  33518  msubrn  33519  onelssex  33689  madebday  34108  imagesset  34283  ivthALT  34552  fness  34566  fneref  34567  refssfne  34575  fnemeet1  34583  fnejoin2  34586  filnetlem2  34596  filnetlem4  34598  ontgval  34648  knoppcnlem10  34710  knoppcnlem11  34711  bj-rabtr  35146  bj-rabtrAUTO  35148  bj-disj2r  35246  bj-restsnid  35286  bj-resta  35295  bj-imdirco  35389  elxp8  35570  finorwe  35581  mblfinlem3  35844  mblfinlem4  35845  ismblfin  35846  ovoliunnfl  35847  voliunnfl  35849  volsupnfl  35850  mbfposadd  35852  ftc1cnnclem  35876  ftc1cnnc  35877  ftc1anc  35886  ftc2nc  35887  areacirclem2  35894  areacirclem4  35896  areacirc  35898  caures  35946  constcncf  35948  brssrid  36646  brcnvssrid  36651  refrelid  36665  n0eldmqs  36787  atpsubN  37793  pol1N  37950  dia2dimlem13  39116  dibord  39199  dochvalr  39397  hdmapevec  39875  lcmineqlem10  40072  lcmineqlem12  40074  eqimssd  40209  ismrcd1  40543  ismrc  40546  incssnn0  40556  mzpclall  40572  rmydioph  40860  rmxdioph  40862  expdiophlem2  40868  expdioph  40869  aomclem6  40908  kelac1  40912  gicabl  40948  arearect  41070  areaquad  41071  clcnvlem  41255  cnvtrcl0  41258  fvilbd  41321  relexp0a  41348  corcltrcl  41371  clsk1indlem2  41676  ntrclskb  41703  wnefimgd  41796  mnuprdlem4  41917  nzss  41959  lhe4.4ex1a  41971  dvsconst  41972  dvsid  41973  dvsef  41974  binomcxplemnn0  41991  onfrALTlem3  42188  onfrALTlem3VD  42531  unisn0  42626  founiiun0  42758  evthiccabs  43069  climconstmpt  43234  cncfshift  43450  addccncf2  43452  cncfcompt  43459  ioccncflimc  43461  icocncflimc  43465  cncfiooicclem1  43469  cncfiooicc  43470  cncfiooiccre  43471  cxpcncf2  43475  add1cncf  43477  add2cncf  43478  sub1cncfd  43479  sub2cncfd  43480  dvcosre  43488  dvmptfprod  43521  ibliooicc  43547  itgsincmulx  43550  itgsubsticclem  43551  itgiccshift  43556  itgperiod  43557  itgsbtaddcnst  43558  dirkeritg  43678  dirkercncflem2  43680  dirkercncflem4  43682  fourierdlem16  43699  fourierdlem18  43701  fourierdlem21  43704  fourierdlem22  43705  fourierdlem23  43706  fourierdlem32  43715  fourierdlem33  43716  fourierdlem39  43722  fourierdlem40  43723  fourierdlem57  43739  fourierdlem58  43740  fourierdlem59  43741  fourierdlem62  43744  fourierdlem68  43750  fourierdlem72  43754  fourierdlem73  43755  fourierdlem74  43756  fourierdlem75  43757  fourierdlem76  43758  fourierdlem78  43760  fourierdlem83  43765  fourierdlem84  43766  fourierdlem85  43767  fourierdlem88  43770  fourierdlem93  43775  fourierdlem94  43776  fourierdlem95  43777  fourierdlem97  43779  fourierdlem101  43783  fourierdlem103  43785  fourierdlem104  43786  fourierdlem111  43793  fourierdlem112  43794  fourierdlem113  43795  sqwvfoura  43804  sqwvfourb  43805  fouriersw  43807  fouriercn  43808  etransclem18  43828  etransclem22  43832  etransclem34  43844  etransclem46  43856  etransclem47  43857  sge0fsum  43961  meaiininclem  44060  hoidmvlelem2  44170  hspdifhsp  44190  hspmbllem2  44201  hspmbl  44203  iinhoiicclem  44247  pimgtmnf2  44288  smflimsuplem1  44393  smflimsuplem6  44398  srhmsubc  45674  srhmsubcALTV  45692