Theorem ssid 3960

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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-ss 3923

This theorem is referenced by:  ssidd  3961  eqimssd  3994  eqimsscd  3995  eqimssi  3998  eqimss2i  3999  nsspssun  4222  difidALT  4334  inv1  4356  disjpss  4422  disjdif  4434  pwidgOLD  4584  elssuni  4905  unimax  4911  intmin  4934  rintn0  5076  sseliALT  5273  inxpssres  5680  xpss1  5682  xpss2  5683  residm  6011  resdm  6027  resmpt3  6042  cnvrescnv  6196  onelssex  6412  ordunidif  6413  funresfunco  6579  dffn3  6720  fdmrn  6739  fvreseq1  7036  iunpw  7771  onsucuni  7825  tfisi  7856  fparlem3  8110  fparlem4  8111  funsssuppss  8187  tfrlem1  8363  tz7.48-2  8430  oaordi  8532  omwordi  8557  omass  8566  nnaordi  8605  nnmwordi  8622  naddunif  8681  fpmg  8867  boxcutc  8940  domss2  9125  findcard2d  9152  fimax2g  9247  domunfican  9282  fipreima  9316  fimin2g  9460  wofib  9508  wemapso  9514  noinfep  9630  cantnfval2  9639  tcidm  9714  tc0  9715  r1rankidb  9777  r1pw  9818  rankr1id  9835  scott0  9861  xpomen  10000  infpwfien  10047  alephsmo  10087  dfac12lem3  10130  cflem  10229  cflemOLD  10230  cflecard  10237  cfslb  10251  fin4en1  10294  fin23lem13  10317  fin23lem36  10333  isf32lem1  10338  fin67  10380  dcomex  10432  zorn2lem4  10484  alephexp2  10567  fpwwe2lem12  10628  canthnumlem  10634  wuncidm  10732  eltsk2g  10737  axgroth6  10814  axgroth3  10817  indconst1  12232  xrsup  13903  expcl  14117  hashcard  14393  hashf1lem2  14495  xptrrel  15019  cotrtrclfv  15051  rtrclreclem2  15098  lo1eq  15621  rlimeq  15622  serclim0  15630  isercolllem2  15719  isercoll  15721  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  fprod2d  16037  risefaccl  16071  fallfaccl  16072  eflt  16174  rpnnen2lem3  16273  rpnnen2lem5  16275  rpnnen2lem12  16282  rexpen  16285  ressbasssg  17298  ressid  17305  ressinbas  17306  oduclatb  18564  ipopos  18593  fpwipodrs  18597  qusxpid  19252  ghmghmrn  19306  elcntr  19401  cntrnsg  19415  0symgefmndeq  19465  sylow3lem5  19702  lsmss1  19736  lsmss2  19738  cmnbascntr  19876  cntrcmnd  19913  cntrabl  19914  gsumzres  19980  gsumzcl2  19981  gsumzf1o  19983  gsumadd  19994  gsumzmhm  20008  gsumzoppg  20015  dprdf1  20106  ablfac1eulem  20145  gsumle  20216  subrgid  20659  srhmsubc  20766  lbsextlem1  21263  rlmval2  21294  znf1o  21682  zntoslem  21687  css0  21820  uvcresum  21924  frlmlbs  21928  psrass1lem  22064  mdetrsca2  22742  mdetrlin2  22745  mdetunilem5  22754  mdetunilem9  22758  smadiadetglem1  22809  smadiadetglem2  22810  pmatcollpw3  22922  topopn  23044  fiinbas  23090  topbas  23110  topcld  23173  ntrtop  23208  opnneissb  23252  opnssneib  23253  opnneiid  23264  maxlp  23285  isperf2  23290  restperf  23322  idcn  23395  cnconst2  23421  lmres  23438  fiuncmp  23542  1stcelcls  23599  ssref  23650  refref  23651  kgencn2  23695  ptpjpre1  23709  ptbasfi  23719  xkopt  23793  elqtop2  23839  ptcmpfi  23951  fbssfi  23975  opnfbas  23980  filtop  23993  isfil2  23994  isfild  23996  fsubbas  24005  ssfg  24010  filssufilg  24049  ufileu  24057  imaelfm  24089  rnelfm  24091  fmfnfmlem4  24095  neiflim  24112  fclscf  24163  flimfnfcls  24166  tsmsfbas  24266  xpsxmet  24518  xpsdsval  24519  xpsmet  24520  tmsxms  24624  tmsms  24625  imasf1oxms  24627  imasf1oms  24628  prdsxms  24668  prdsms  24669  tmsxpsval  24676  retopbas  24898  cnngp  24917  cnopn  24924  cnperf  24959  retopconn  24968  fsumcn  25010  abscncf  25041  recncf  25042  imcncf  25043  cjcncf  25044  mulc1cncf  25045  cncfcn1  25051  cncfmpt2f  25055  cncfmpt2ss  25056  addccncf  25057  idcncf  25058  sub1cncf  25059  sub2cncf  25060  cdivcncf  25061  negcncf  25062  negfcncf  25063  abscncfALT  25064  cnmpopc  25068  xrhmeo  25086  oprpiece1res1  25091  oprpiece1res2  25092  cnrehmeo  25093  iscau3  25418  caubl  25448  caublcls  25449  mulcncf  25586  evthicc2  25600  ovolre  25665  volsuplem  25695  uniiccdif  25718  uniioovol  25719  uniiccvol  25720  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  dyadmbllem  25739  volivth  25747  itgfsum  25967  iblabslem  25968  iblabs  25969  bddmulibl  25979  cnlimc  26028  cnlimci  26029  dvcnp2  26060  dvcn  26061  cpnord  26075  cpnres  26077  dvmptntr  26111  dvmptfsum  26115  rolle  26130  dvlipcn  26134  c1liplem1  26136  dvivth  26150  dvfsumabs  26163  ftc1a  26177  ftc1cn  26183  plyssc  26338  plyeq0  26349  0dgr  26383  coemulc  26393  coe0  26394  coesub  26395  coe1termlem  26396  dgrmulc  26409  dgrsub  26410  dvnply2  26429  plycpn  26431  plyremlem  26446  fta1lem  26449  vieta1lem2  26453  aalioulem3  26478  taylthlem1  26517  taylthlem2  26518  ulmcn  26543  psercn  26570  abelth  26585  efcn  26587  efcvx  26593  dvrelog  26783  logcn  26793  dvloglem  26794  dvlog  26797  dvlog2  26799  efopnlem2  26803  logccv  26809  cxpcn  26891  cxpcn3  26894  resqrtcn  26895  sqrtcn  26896  loglesqrt  26907  atancn  27082  jensen  27134  ftalem3  27220  dchrfi  27400  dchrisumlema  27633  pntlem3  27754  madebday  28074  expscl  28605  bdaypw2n0bndlem  28637  uhgrsubgrself  29611  uhgrspansubgr  29622  umgr2adedgwlk  30275  umgr2adedgwlkon  30276  umgr2adedgspth  30278  upgr1wlkdlem2  30478  sspid  31058  ssps  31063  helch  31576  hhssnv  31597  hhsssh  31602  shintcl  31663  chintcl  31665  shlesb1i  31719  omlsi  31737  chlejb1i  31809  chm0i  31823  chabs1  31849  chabs2  31850  spanun  31878  cmidi  31943  pjidmcoi  32510  csmdsymi  32667  sumdmdlem2  32752  dmdbr5ati  32755  mdcompli  32762  dmdcompli  32763  disjdifprg  32901  fcoinver  32930  f1rnen  32954  xppreima  32971  padct  33044  xrinfm  33081  clatp0cl  33277  clatp1cl  33278  xrsp0  33313  xrsp1  33314  cntrcrng  33382  cycpmconjslem1  33455  cycpmconjslem2  33456  gsumvsca1  33527  gsumvsca2  33528  ellspds  33664  rspidlid  33670  rlmdim  33981  reff  34210  locfinreflem  34211  esumsnf  34435  esumcvg  34457  sigagenid  34522  iblidicc  34960  cxpcncf1  34963  fdvposlt  34967  fdvneggt  34968  fdvposle  34969  fdvnegge  34970  logdivsqrle  35018  bnj1253  35386  fineqvac  35510  fineqvnttrclse  35518  noinfepfnregs  35526  cvmlift2lem6  35781  satfun  35884  mrsubrn  35986  elmrsubrn  35993  elmsubrn  36001  msubrn  36002  imagesset  36426  nmuladdss  36671  ivthALT  36827  fness  36841  fneref  36842  refssfne  36850  fnemeet1  36858  fnejoin2  36861  filnetlem2  36871  filnetlem4  36873  ontgval  36923  ttctrid  36994  knoppcnlem10  37072  knoppcnlem11  37073  bj-rabtr  37547  bj-rabtrAUTO  37549  bj-disj2r  37645  bj-restsnid  37710  bj-resta  37719  bj-imdirco  37815  elxp8  37998  finorwe  38009  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  mbfposadd  38299  ftc1cnnclem  38323  ftc1cnnc  38324  ftc1anc  38333  ftc2nc  38334  areacirclem2  38341  areacirclem4  38343  areacirc  38345  caures  38392  constcncf  38394  brssrid  39212  brcnvssrid  39217  refrelid  39232  n0eldmqs  39362  atpsubN  40508  pol1N  40665  dia2dimlem13  41831  dibord  41914  dochvalr  42112  hdmapevec  42590  lcmineqlem10  42786  lcmineqlem12  42788  ismrcd1  43412  ismrc  43415  incssnn0  43425  mzpclall  43441  rmydioph  43724  rmxdioph  43726  expdiophlem2  43732  expdioph  43733  aomclem6  43769  kelac1  43773  gicabl  43809  arearect  43925  areaquad  43926  unielid  43929  oege2  44017  oacl2g  44040  ofoaf  44065  clcnvlem  44332  cnvtrcl0  44335  fvilbd  44398  relexp0a  44425  corcltrcl  44448  clsk1indlem2  44751  ntrclskb  44778  wnefimgd  44870  mnuprdlem4  44968  nzss  45010  lhe4.4ex1a  45022  dvsconst  45023  dvsid  45024  dvsef  45025  binomcxplemnn0  45042  onfrALTlem3  45236  onfrALTlem3VD  45578  unisn0  45757  founiiun0  45891  evthiccabs  46195  climconstmpt  46355  cncfshift  46571  addccncf2  46573  cncfcompt  46580  ioccncflimc  46582  icocncflimc  46586  cncfiooicclem1  46590  cncfiooicc  46591  cncfiooiccre  46592  cxpcncf2  46596  add1cncf  46598  add2cncf  46599  sub1cncfd  46600  sub2cncfd  46601  dvcosre  46609  dvmptfprod  46642  ibliooicc  46668  itgsincmulx  46671  itgsubsticclem  46672  itgiccshift  46677  itgperiod  46678  itgsbtaddcnst  46679  dirkeritg  46799  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem16  46820  fourierdlem18  46822  fourierdlem21  46825  fourierdlem22  46826  fourierdlem23  46827  fourierdlem32  46836  fourierdlem33  46837  fourierdlem39  46843  fourierdlem40  46844  fourierdlem57  46860  fourierdlem58  46861  fourierdlem59  46862  fourierdlem62  46865  fourierdlem68  46871  fourierdlem72  46875  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem78  46881  fourierdlem83  46886  fourierdlem84  46887  fourierdlem85  46888  fourierdlem88  46891  fourierdlem93  46896  fourierdlem94  46897  fourierdlem95  46898  fourierdlem97  46900  fourierdlem101  46904  fourierdlem103  46906  fourierdlem104  46907  fourierdlem111  46914  fourierdlem112  46915  sqwvfoura  46925  sqwvfourb  46926  fouriersw  46928  fouriercn  46929  etransclem18  46949  etransclem22  46953  etransclem34  46965  etransclem46  46977  etransclem47  46978  sge0fsum  47084  meaiininclem  47183  hoidmvlelem2  47293  hspdifhsp  47313  hspmbllem2  47324  hspmbl  47326  iinhoiicclem  47370  pimgtmnf2  47411  smflimsuplem1  47517  smflimsuplem6  47522  cjnpoly  47609  srhmsubcALTV  49073  imaidfu2lem  49870  imaidfu  49871  imaidfu2  49872  setc1onsubc  50363