Theorem ssid 3972

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3917

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

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

This theorem is referenced by:  ssidd  3973  eqimssd  4006  eqimsscd  4007  eqimssi  4010  eqimss2i  4011  nsspssun  4234  difidALT  4343  inv1  4364  disjpss  4427  pwidg  4586  elssuni  4904  unimax  4911  intmin  4935  rintn0  5076  sseliALT  5267  inxpssres  5658  xpss1  5660  xpss2  5661  residm  5984  resdm  6000  resmpt3  6012  cnvrescnv  6171  onelssex  6384  ordunidif  6385  funresfunco  6560  dffn3  6703  fdmrn  6722  fvreseq1  7014  iunpw  7750  onsucuni  7806  tfisi  7838  fparlem3  8096  fparlem4  8097  funsssuppss  8172  tfrlem1  8347  tz7.48-2  8413  oaordi  8513  omwordi  8538  omass  8547  nnaordi  8585  nnmwordi  8602  naddunif  8660  fpmg  8844  boxcutc  8917  domss2  9106  findcard2d  9136  0finOLD  9140  en1eqsnOLD  9227  fimax2g  9240  domunfican  9279  fipreima  9316  fimin2g  9457  wofib  9505  wemapso  9511  noinfep  9620  cantnfval2  9629  tcidm  9706  tc0  9707  r1rankidb  9764  r1pw  9805  rankr1id  9822  scott0  9846  xpomen  9975  infpwfien  10022  alephsmo  10062  dfac12lem3  10106  cflem  10205  cflemOLD  10206  cflecard  10213  cfslb  10226  fin4en1  10269  fin23lem13  10292  fin23lem36  10308  isf32lem1  10313  fin67  10355  dcomex  10407  zorn2lem4  10459  alephexp2  10541  fpwwe2lem12  10602  canthnumlem  10608  wuncidm  10706  eltsk2g  10711  axgroth6  10788  axgroth3  10791  xrsup  13837  expcl  14051  hashcard  14327  hashf1lem2  14428  xptrrel  14953  cotrtrclfv  14985  rtrclreclem2  15032  lo1eq  15541  rlimeq  15542  serclim0  15550  isercolllem2  15639  isercoll  15641  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  fprod2d  15954  risefaccl  15988  fallfaccl  15989  eflt  16092  rpnnen2lem3  16191  rpnnen2lem5  16193  rpnnen2lem12  16200  rexpen  16203  ressbasssg  17214  ressid  17221  ressinbas  17222  oduclatb  18473  ipopos  18502  fpwipodrs  18506  ghmghmrn  19174  elcntr  19269  cntrnsg  19283  0symgefmndeq  19331  sylow3lem5  19568  lsmss1  19602  lsmss2  19604  cmnbascntr  19742  cntrcmnd  19779  cntrabl  19780  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumadd  19860  gsumzmhm  19874  gsumzoppg  19881  dprdf1  19972  ablfac1eulem  20011  subrgid  20489  srhmsubc  20596  lbsextlem1  21075  rlmval2  21106  znf1o  21468  zntoslem  21473  css0  21605  uvcresum  21709  frlmlbs  21713  psrass1lem  21848  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  mdetunilem9  22514  smadiadetglem1  22565  smadiadetglem2  22566  pmatcollpw3  22678  topopn  22800  fiinbas  22846  topbas  22866  topcld  22929  ntrtop  22964  opnneissb  23008  opnssneib  23009  opnneiid  23020  maxlp  23041  isperf2  23046  restperf  23078  idcn  23151  cnconst2  23177  lmres  23194  fiuncmp  23298  1stcelcls  23355  ssref  23406  refref  23407  kgencn2  23451  ptpjpre1  23465  ptbasfi  23475  xkopt  23549  elqtop2  23595  ptcmpfi  23707  fbssfi  23731  opnfbas  23736  filtop  23749  isfil2  23750  isfild  23752  fsubbas  23761  ssfg  23766  filssufilg  23805  ufileu  23813  imaelfm  23845  rnelfm  23847  fmfnfmlem4  23851  neiflim  23868  fclscf  23919  flimfnfcls  23922  tsmsfbas  24022  xpsxmet  24275  xpsdsval  24276  xpsmet  24277  tmsxms  24381  tmsms  24382  imasf1oxms  24384  imasf1oms  24385  prdsxms  24425  prdsms  24426  tmsxpsval  24433  retopbas  24655  cnngp  24674  cnopn  24681  cnperf  24716  retopconn  24725  fsumcn  24768  abscncf  24801  recncf  24802  imcncf  24803  cjcncf  24804  mulc1cncf  24805  cncfcn1  24811  cncfmpt2f  24815  cncfmpt2ss  24816  addccncf  24817  idcncf  24818  sub1cncf  24819  sub2cncf  24820  cdivcncf  24821  negcncf  24822  negcncfOLD  24823  negfcncf  24824  abscncfALT  24825  cnmpopc  24829  xrhmeo  24851  oprpiece1res1  24856  oprpiece1res2  24857  cnrehmeo  24858  cnrehmeoOLD  24859  iscau3  25185  caubl  25215  caublcls  25216  mulcncf  25353  evthicc2  25368  ovolre  25433  volsuplem  25463  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  dyadmbllem  25507  volivth  25515  itgfsum  25735  iblabslem  25736  iblabs  25737  bddmulibl  25747  cnlimc  25796  cnlimci  25797  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  cpnord  25844  cpnres  25846  dvmptntr  25882  dvmptfsum  25886  rolle  25901  dvlipcn  25906  c1liplem1  25908  dvivth  25922  dvfsumabs  25936  ftc1a  25951  ftc1cn  25957  plyssc  26112  plyeq0  26123  0dgr  26157  coemulc  26167  coe0  26168  coesub  26169  coe1termlem  26170  dgrmulc  26184  dgrsub  26185  dvnply2  26202  plycpn  26204  plyremlem  26219  fta1lem  26222  vieta1lem2  26226  aalioulem3  26249  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmcn  26315  psercn  26343  abelth  26358  efcn  26360  efcvx  26366  dvrelog  26553  logcn  26563  dvloglem  26564  dvlog  26567  dvlog2  26569  efopnlem2  26573  logccv  26579  cxpcn  26661  cxpcnOLD  26662  cxpcn3  26665  resqrtcn  26666  sqrtcn  26667  loglesqrt  26678  atancn  26853  jensen  26906  ftalem3  26992  dchrfi  27173  dchrisumlema  27406  pntlem3  27527  madebday  27818  expscl  28324  uhgrsubgrself  29214  uhgrspansubgr  29225  umgr2adedgwlk  29882  umgr2adedgwlkon  29883  umgr2adedgspth  29885  upgr1wlkdlem2  30082  sspid  30661  ssps  30666  helch  31179  hhssnv  31200  hhsssh  31205  shintcl  31266  chintcl  31268  shlesb1i  31322  omlsi  31340  chlejb1i  31412  chm0i  31426  chabs1  31452  chabs2  31453  spanun  31481  cmidi  31546  pjidmcoi  32113  csmdsymi  32270  sumdmdlem2  32355  dmdbr5ati  32358  mdcompli  32365  dmdcompli  32366  disjdifprg  32511  fcoinver  32540  f1rnen  32560  xppreima  32576  padct  32650  xrinfm  32685  clatp0cl  32909  clatp1cl  32910  xrsp0  32957  xrsp1  32958  cntrcrng  33017  gsumle  33045  cycpmconjslem1  33118  cycpmconjslem2  33119  gsumvsca1  33186  gsumvsca2  33187  qusxpid  33341  ellspds  33346  rspidlid  33353  rlmdim  33612  reff  33836  locfinreflem  33837  esumsnf  34061  esumcvg  34083  sigagenid  34148  iblidicc  34590  cxpcncf1  34593  fdvposlt  34597  fdvneggt  34598  fdvposle  34599  fdvnegge  34600  logdivsqrle  34648  bnj1253  35014  fineqvac  35094  cvmlift2lem6  35302  satfun  35405  mrsubrn  35507  elmrsubrn  35514  elmsubrn  35522  msubrn  35523  imagesset  35948  ivthALT  36330  fness  36344  fneref  36345  refssfne  36353  fnemeet1  36361  fnejoin2  36364  filnetlem2  36374  filnetlem4  36376  ontgval  36426  knoppcnlem10  36497  knoppcnlem11  36498  bj-rabtr  36925  bj-rabtrAUTO  36927  bj-disj2r  37023  bj-restsnid  37082  bj-resta  37091  bj-imdirco  37185  elxp8  37366  finorwe  37377  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfposadd  37668  ftc1cnnclem  37692  ftc1cnnc  37693  ftc1anc  37702  ftc2nc  37703  areacirclem2  37710  areacirclem4  37712  areacirc  37714  caures  37761  constcncf  37763  brssrid  38500  brcnvssrid  38505  refrelid  38520  n0eldmqs  38646  atpsubN  39754  pol1N  39911  dia2dimlem13  41077  dibord  41160  dochvalr  41358  hdmapevec  41836  lcmineqlem10  42033  lcmineqlem12  42035  ismrcd1  42693  ismrc  42696  incssnn0  42706  mzpclall  42722  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  aomclem6  43055  kelac1  43059  gicabl  43095  arearect  43211  areaquad  43212  unielid  43215  oege2  43303  oacl2g  43326  ofoaf  43351  clcnvlem  43619  cnvtrcl0  43622  fvilbd  43685  relexp0a  43712  corcltrcl  43735  clsk1indlem2  44038  ntrclskb  44065  wnefimgd  44157  mnuprdlem4  44271  nzss  44313  lhe4.4ex1a  44325  dvsconst  44326  dvsid  44327  dvsef  44328  binomcxplemnn0  44345  onfrALTlem3  44541  onfrALTlem3VD  44883  unisn0  45055  founiiun0  45191  evthiccabs  45501  climconstmpt  45663  cncfshift  45879  addccncf2  45881  cncfcompt  45888  ioccncflimc  45890  icocncflimc  45894  cncfiooicclem1  45898  cncfiooicc  45899  cncfiooiccre  45900  cxpcncf2  45904  add1cncf  45906  add2cncf  45907  sub1cncfd  45908  sub2cncfd  45909  dvcosre  45917  dvmptfprod  45950  ibliooicc  45976  itgsincmulx  45979  itgsubsticclem  45980  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem16  46128  fourierdlem18  46130  fourierdlem21  46133  fourierdlem22  46134  fourierdlem23  46135  fourierdlem32  46144  fourierdlem33  46145  fourierdlem39  46151  fourierdlem40  46152  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem62  46173  fourierdlem68  46179  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem83  46194  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem93  46204  fourierdlem94  46205  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  fouriercn  46237  etransclem18  46257  etransclem22  46261  etransclem34  46273  etransclem46  46285  etransclem47  46286  sge0fsum  46392  meaiininclem  46491  hoidmvlelem2  46601  hspdifhsp  46621  hspmbllem2  46632  hspmbl  46634  iinhoiicclem  46678  pimgtmnf2  46719  smflimsuplem1  46825  smflimsuplem6  46830  srhmsubcALTV  48317  imaidfu2lem  49102  imaidfu  49103  imaidfu2  49104  setc1onsubc  49595