Theorem ssid 3944

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

Syntax hints:   ∈ wcel 2119   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 208  df-ss 3907

This theorem is referenced by:  ssidd  3945  eqimssd  3978  eqimsscd  3979  eqimssi  3982  eqimss2i  3983  nsspssun  4203  difidALT  4312  inv1  4333  disjpss  4396  pwidg  4556  elssuni  4876  unimax  4882  intmin  4905  rintn0  5045  sseliALT  5238  inxpssres  5642  xpss1  5644  xpss2  5645  residm  5969  resdm  5985  resmpt3  5997  cnvrescnv  6153  onelssex  6366  ordunidif  6367  funresfunco  6533  dffn3  6674  fdmrn  6693  fvreseq1  6987  iunpw  7721  onsucuni  7775  tfisi  7806  fparlem3  8060  fparlem4  8061  funsssuppss  8137  tfrlem1  8312  tz7.48-2  8378  oaordi  8478  omwordi  8503  omass  8512  nnaordi  8551  nnmwordi  8568  naddunif  8626  fpmg  8813  boxcutc  8886  domss2  9071  findcard2d  9098  fimax2g  9193  domunfican  9229  fipreima  9265  fimin2g  9409  wofib  9457  wemapso  9463  noinfep  9579  cantnfval2  9588  tcidm  9663  tc0  9664  r1rankidb  9726  r1pw  9767  rankr1id  9784  scott0  9808  xpomen  9935  infpwfien  9982  alephsmo  10022  dfac12lem3  10066  cflem  10165  cflemOLD  10166  cflecard  10173  cfslb  10186  fin4en1  10229  fin23lem13  10252  fin23lem36  10268  isf32lem1  10273  fin67  10315  dcomex  10367  zorn2lem4  10419  alephexp2  10502  fpwwe2lem12  10563  canthnumlem  10569  wuncidm  10667  eltsk2g  10672  axgroth6  10749  axgroth3  10752  indconst1  12170  xrsup  13825  expcl  14039  hashcard  14315  hashf1lem2  14416  xptrrel  14940  cotrtrclfv  14972  rtrclreclem2  15019  lo1eq  15528  rlimeq  15529  serclim0  15537  isercolllem2  15626  isercoll  15628  fsum2d  15731  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  fprod2d  15944  risefaccl  15978  fallfaccl  15979  eflt  16082  rpnnen2lem3  16181  rpnnen2lem5  16183  rpnnen2lem12  16190  rexpen  16193  ressbasssg  17205  ressid  17212  ressinbas  17213  oduclatb  18471  ipopos  18500  fpwipodrs  18504  ghmghmrn  19208  elcntr  19303  cntrnsg  19317  0symgefmndeq  19367  sylow3lem5  19604  lsmss1  19638  lsmss2  19640  cmnbascntr  19778  cntrcmnd  19815  cntrabl  19816  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumadd  19896  gsumzmhm  19910  gsumzoppg  19917  dprdf1  20008  ablfac1eulem  20047  gsumle  20118  subrgid  20552  srhmsubc  20659  lbsextlem1  21158  rlmval2  21189  znf1o  21533  zntoslem  21538  css0  21671  uvcresum  21775  frlmlbs  21779  psrass1lem  21915  mdetrsca2  22594  mdetrlin2  22597  mdetunilem5  22606  mdetunilem9  22610  smadiadetglem1  22661  smadiadetglem2  22662  pmatcollpw3  22774  topopn  22896  fiinbas  22942  topbas  22962  topcld  23025  ntrtop  23060  opnneissb  23104  opnssneib  23105  opnneiid  23116  maxlp  23137  isperf2  23142  restperf  23174  idcn  23247  cnconst2  23273  lmres  23290  fiuncmp  23394  1stcelcls  23451  ssref  23502  refref  23503  kgencn2  23547  ptpjpre1  23561  ptbasfi  23571  xkopt  23645  elqtop2  23691  ptcmpfi  23803  fbssfi  23827  opnfbas  23832  filtop  23845  isfil2  23846  isfild  23848  fsubbas  23857  ssfg  23862  filssufilg  23901  ufileu  23909  imaelfm  23941  rnelfm  23943  fmfnfmlem4  23947  neiflim  23964  fclscf  24015  flimfnfcls  24018  tsmsfbas  24118  xpsxmet  24370  xpsdsval  24371  xpsmet  24372  tmsxms  24476  tmsms  24477  imasf1oxms  24479  imasf1oms  24480  prdsxms  24520  prdsms  24521  tmsxpsval  24528  retopbas  24750  cnngp  24769  cnopn  24776  cnperf  24811  retopconn  24820  fsumcn  24862  abscncf  24893  recncf  24894  imcncf  24895  cjcncf  24896  mulc1cncf  24897  cncfcn1  24903  cncfmpt2f  24907  cncfmpt2ss  24908  addccncf  24909  idcncf  24910  sub1cncf  24911  sub2cncf  24912  cdivcncf  24913  negcncf  24914  negfcncf  24915  abscncfALT  24916  cnmpopc  24920  xrhmeo  24938  oprpiece1res1  24943  oprpiece1res2  24944  cnrehmeo  24945  iscau3  25270  caubl  25300  caublcls  25301  mulcncf  25438  evthicc2  25452  ovolre  25517  volsuplem  25547  uniiccdif  25570  uniioovol  25571  uniiccvol  25572  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  dyadmbllem  25591  volivth  25599  itgfsum  25819  iblabslem  25820  iblabs  25821  bddmulibl  25831  cnlimc  25880  cnlimci  25881  dvcnp2  25912  dvcn  25913  cpnord  25927  cpnres  25929  dvmptntr  25963  dvmptfsum  25967  rolle  25982  dvlipcn  25986  c1liplem1  25988  dvivth  26002  dvfsumabs  26015  ftc1a  26029  ftc1cn  26035  plyssc  26190  plyeq0  26201  0dgr  26235  coemulc  26245  coe0  26246  coesub  26247  coe1termlem  26248  dgrmulc  26261  dgrsub  26262  dvnply2  26278  plycpn  26280  plyremlem  26295  fta1lem  26298  vieta1lem2  26302  aalioulem3  26325  taylthlem1  26363  taylthlem2  26364  ulmcn  26389  psercn  26416  abelth  26431  efcn  26433  efcvx  26439  dvrelog  26626  logcn  26636  dvloglem  26637  dvlog  26640  dvlog2  26642  efopnlem2  26646  logccv  26652  cxpcn  26734  cxpcn3  26737  resqrtcn  26738  sqrtcn  26739  loglesqrt  26750  atancn  26925  jensen  26977  ftalem3  27063  dchrfi  27243  dchrisumlema  27476  pntlem3  27597  madebday  27917  expscl  28448  bdaypw2n0bndlem  28480  uhgrsubgrself  29374  uhgrspansubgr  29385  umgr2adedgwlk  30038  umgr2adedgwlkon  30039  umgr2adedgspth  30041  upgr1wlkdlem2  30241  sspid  30821  ssps  30826  helch  31339  hhssnv  31360  hhsssh  31365  shintcl  31426  chintcl  31428  shlesb1i  31482  omlsi  31500  chlejb1i  31572  chm0i  31586  chabs1  31612  chabs2  31613  spanun  31641  cmidi  31706  pjidmcoi  32273  csmdsymi  32430  sumdmdlem2  32515  dmdbr5ati  32518  mdcompli  32525  dmdcompli  32526  disjdifprg  32671  fcoinver  32700  f1rnen  32727  xppreima  32744  padct  32817  xrinfm  32854  clatp0cl  33062  clatp1cl  33063  xrsp0  33098  xrsp1  33099  cntrcrng  33169  cycpmconjslem1  33242  cycpmconjslem2  33243  gsumvsca1  33314  gsumvsca2  33315  qusxpid  33453  ellspds  33458  rspidlid  33465  rlmdim  33801  reff  34030  locfinreflem  34031  esumsnf  34255  esumcvg  34277  sigagenid  34342  iblidicc  34783  cxpcncf1  34786  fdvposlt  34790  fdvneggt  34791  fdvposle  34792  fdvnegge  34793  logdivsqrle  34841  bnj1253  35206  fineqvac  35304  fineqvnttrclse  35312  noinfepfnregs  35320  cvmlift2lem6  35543  satfun  35646  mrsubrn  35748  elmrsubrn  35755  elmsubrn  35763  msubrn  35764  imagesset  36188  ivthALT  36570  fness  36584  fneref  36585  refssfne  36593  fnemeet1  36601  fnejoin2  36604  filnetlem2  36614  filnetlem4  36616  ontgval  36666  ttctrid  36737  knoppcnlem10  36815  knoppcnlem11  36816  bj-rabtr  37290  bj-rabtrAUTO  37292  bj-disj2r  37388  bj-restsnid  37452  bj-resta  37461  bj-imdirco  37557  elxp8  37740  finorwe  37751  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  mbfposadd  38041  ftc1cnnclem  38065  ftc1cnnc  38066  ftc1anc  38075  ftc2nc  38076  areacirclem2  38083  areacirclem4  38085  areacirc  38087  caures  38134  constcncf  38136  brssrid  38956  brcnvssrid  38961  refrelid  38976  n0eldmqs  39106  atpsubN  40252  pol1N  40409  dia2dimlem13  41575  dibord  41658  dochvalr  41856  hdmapevec  42334  lcmineqlem10  42530  lcmineqlem12  42532  ismrcd1  43154  ismrc  43157  incssnn0  43167  mzpclall  43183  rmydioph  43466  rmxdioph  43468  expdiophlem2  43474  expdioph  43475  aomclem6  43511  kelac1  43515  gicabl  43551  arearect  43667  areaquad  43668  unielid  43671  oege2  43759  oacl2g  43782  ofoaf  43807  clcnvlem  44074  cnvtrcl0  44077  fvilbd  44140  relexp0a  44167  corcltrcl  44190  clsk1indlem2  44493  ntrclskb  44520  wnefimgd  44612  mnuprdlem4  44726  nzss  44768  lhe4.4ex1a  44780  dvsconst  44781  dvsid  44782  dvsef  44783  binomcxplemnn0  44800  onfrALTlem3  44995  onfrALTlem3VD  45337  unisn0  45509  founiiun0  45644  evthiccabs  45948  climconstmpt  46108  cncfshift  46324  addccncf2  46326  cncfcompt  46333  ioccncflimc  46335  icocncflimc  46339  cncfiooicclem1  46343  cncfiooicc  46344  cncfiooiccre  46345  cxpcncf2  46349  add1cncf  46351  add2cncf  46352  sub1cncfd  46353  sub2cncfd  46354  dvcosre  46362  dvmptfprod  46395  ibliooicc  46421  itgsincmulx  46424  itgsubsticclem  46425  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  dirkeritg  46552  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem16  46573  fourierdlem18  46575  fourierdlem21  46578  fourierdlem22  46579  fourierdlem23  46580  fourierdlem32  46589  fourierdlem33  46590  fourierdlem39  46596  fourierdlem40  46597  fourierdlem57  46613  fourierdlem58  46614  fourierdlem59  46615  fourierdlem62  46618  fourierdlem68  46624  fourierdlem72  46628  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem83  46639  fourierdlem84  46640  fourierdlem85  46641  fourierdlem88  46644  fourierdlem93  46649  fourierdlem94  46650  fourierdlem95  46651  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  fouriercn  46682  etransclem18  46702  etransclem22  46706  etransclem34  46718  etransclem46  46730  etransclem47  46731  sge0fsum  46837  meaiininclem  46936  hoidmvlelem2  47046  hspdifhsp  47066  hspmbllem2  47077  hspmbl  47079  iinhoiicclem  47123  pimgtmnf2  47164  smflimsuplem1  47270  smflimsuplem6  47275  cjnpoly  47359  srhmsubcALTV  48823  imaidfu2lem  49606  imaidfu  49607  imaidfu2  49608  setc1onsubc  50099