Theorem ssid 3915

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

Syntax hints:   ∈ wcel 2112   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876

This theorem is referenced by:  ssidd  3916  eqimssi  3951  eqimss2i  3952  nsspssun  4163  difidALT  4271  inv1  4291  disjpss  4358  pwidg  4517  elssuni  4831  unimax  4837  intmin  4859  rintn0  4997  sseliALT  5180  inxpssres  5542  xpss1  5544  xpss2  5545  residm  5857  resdm  5869  resmpt3  5879  cnvrescnv  6025  ordunidif  6218  funresfunco  6377  dffn3  6511  fdmrn  6524  fvreseq1  6801  fimacnv  6831  iunpw  7493  onsucuni  7543  tfisi  7573  fparlem3  7815  fparlem4  7816  funsssuppss  7865  tfrlem1  8023  tz7.48-2  8089  oaordi  8183  omwordi  8208  omass  8217  nnaordi  8255  nnmwordi  8272  fpmg  8451  boxcutc  8524  domss2  8699  findcard2d  8738  0fin  8741  en1eqsn  8785  fimax2g  8798  domunfican  8825  pwfiOLD  8853  fipreima  8864  fimin2g  8995  wofib  9043  wemapso  9049  noinfep  9157  cantnfval2  9166  tcidm  9222  tc0  9223  r1rankidb  9267  r1pw  9308  rankr1id  9325  scott0  9349  xpomen  9476  infpwfien  9523  alephsmo  9563  dfac12lem3  9606  cflem  9707  cflecard  9714  cfslb  9727  fin4en1  9770  fin23lem13  9793  fin23lem36  9809  isf32lem1  9814  fin67  9856  dcomex  9908  zorn2lem4  9960  alephexp2  10042  fpwwe2lem12  10103  canthnumlem  10109  wuncidm  10207  eltsk2g  10212  axgroth6  10289  axgroth3  10292  xrsup  13286  expcl  13498  hashcard  13767  hashf1lem2  13867  xptrrel  14388  cotrtrclfv  14420  rtrclreclem2  14467  lo1eq  14974  rlimeq  14975  serclim0  14983  isercolllem2  15071  isercoll  15073  fsum2d  15175  fsumabs  15205  fsumrlim  15215  fsumo1  15216  fsumiun  15225  fprod2d  15384  risefaccl  15418  fallfaccl  15419  eflt  15519  rpnnen2lem3  15618  rpnnen2lem5  15620  rpnnen2lem12  15627  rexpen  15630  ressid  16618  ressinbas  16619  oduclatb  17821  ipopos  17837  fpwipodrs  17841  ghmghmrn  18445  cntrnsg  18540  0symgefmndeq  18590  sylow3lem5  18824  lsmss1  18859  lsmss2  18861  cntrcmnd  19031  cntrabl  19032  gsumzres  19098  gsumzcl2  19099  gsumzf1o  19101  gsumadd  19112  gsumzmhm  19126  gsumzoppg  19133  dprdf1  19224  ablfac1eulem  19263  subrgid  19606  lbsextlem1  19999  rlmval2  20035  znf1o  20320  zntoslem  20325  css0  20455  uvcresum  20559  frlmlbs  20563  psrass1lemOLD  20703  psrass1lem  20706  mdetrsca2  21305  mdetrlin2  21308  mdetunilem5  21317  mdetunilem9  21321  smadiadetglem1  21372  smadiadetglem2  21373  pmatcollpw3  21485  topopn  21607  fiinbas  21653  topbas  21673  topcld  21736  ntrtop  21771  opnneissb  21815  opnssneib  21816  opnneiid  21827  maxlp  21848  isperf2  21853  restperf  21885  idcn  21958  cnconst2  21984  lmres  22001  fiuncmp  22105  1stcelcls  22162  ssref  22213  refref  22214  kgencn2  22258  ptpjpre1  22272  ptbasfi  22282  xkopt  22356  elqtop2  22402  ptcmpfi  22514  fbssfi  22538  opnfbas  22543  filtop  22556  isfil2  22557  isfild  22559  fsubbas  22568  ssfg  22573  filssufilg  22612  ufileu  22620  imaelfm  22652  rnelfm  22654  fmfnfmlem4  22658  neiflim  22675  fclscf  22726  flimfnfcls  22729  tsmsfbas  22829  xpsxmet  23083  xpsdsval  23084  xpsmet  23085  tmsxms  23189  tmsms  23190  imasf1oxms  23192  imasf1oms  23193  prdsxms  23233  prdsms  23234  tmsxpsval  23241  retopbas  23463  cnngp  23482  cnopn  23489  cnperf  23522  retopconn  23531  fsumcn  23572  abscncf  23603  recncf  23604  imcncf  23605  cjcncf  23606  mulc1cncf  23607  cncfcn1  23613  cncfmpt2f  23617  cncfmpt2ss  23618  addccncf  23619  idcncf  23620  sub1cncf  23621  sub2cncf  23622  cdivcncf  23623  negcncf  23624  negfcncf  23625  abscncfALT  23626  cnmpopc  23630  xrhmeo  23648  oprpiece1res1  23653  oprpiece1res2  23654  cnrehmeo  23655  iscau3  23979  caubl  24009  caublcls  24010  evthicc2  24161  ovolre  24226  volsuplem  24256  uniiccdif  24279  uniioovol  24280  uniiccvol  24281  uniioombllem3  24286  uniioombllem4  24287  uniioombllem5  24288  dyadmbllem  24300  volivth  24308  itgfsum  24527  iblabslem  24528  iblabs  24529  bddmulibl  24539  cnlimc  24588  cnlimci  24589  dvcnp2  24620  dvcn  24621  cpnord  24635  cpnres  24637  dvmptntr  24671  dvmptfsum  24675  rolle  24690  dvlipcn  24694  c1liplem1  24696  dvivth  24710  dvfsumabs  24723  ftc1a  24737  ftc1cn  24743  plyssc  24897  plyeq0  24908  0dgr  24942  coemulc  24952  coe0  24953  coesub  24954  coe1termlem  24955  dgrmulc  24968  dgrsub  24969  dvnply2  24983  plycpn  24985  plyremlem  25000  fta1lem  25003  vieta1lem2  25007  aalioulem3  25030  taylthlem1  25068  taylthlem2  25069  ulmcn  25094  psercn  25121  abelth  25136  efcn  25138  efcvx  25144  dvrelog  25328  logcn  25338  dvloglem  25339  dvlog  25342  dvlog2  25344  efopnlem2  25348  logccv  25354  cxpcn  25434  cxpcn3  25437  resqrtcn  25438  sqrtcn  25439  loglesqrt  25447  atancn  25622  jensen  25674  ftalem3  25760  dchrfi  25939  dchrisumlema  26172  pntlem3  26293  uhgrsubgrself  27170  uhgrspansubgr  27181  umgr2adedgwlk  27831  umgr2adedgwlkon  27832  umgr2adedgspth  27834  upgr1wlkdlem2  28031  sspid  28608  ssps  28613  helch  29126  hhssnv  29147  hhsssh  29152  shintcl  29213  chintcl  29215  shlesb1i  29269  omlsi  29287  chlejb1i  29359  chm0i  29373  chabs1  29399  chabs2  29400  spanun  29428  cmidi  29493  pjidmcoi  30060  csmdsymi  30217  sumdmdlem2  30302  dmdbr5ati  30305  mdcompli  30312  dmdcompli  30313  disjdifprg  30437  fcoinver  30469  f1rnen  30487  xppreima  30507  padct  30579  xrinfm  30602  clatp0cl  30781  clatp1cl  30782  xrsp0  30817  xrsp1  30818  cntrcrng  30849  gsumle  30877  cycpmconjslem1  30948  cycpmconjslem2  30949  gsumvsca1  31006  gsumvsca2  31007  qusxpid  31081  ellspds  31086  rspidlid  31092  reff  31311  locfinreflem  31312  esumsnf  31552  esumcvg  31574  sigagenid  31639  iblidicc  32092  cxpcncf1  32095  fdvposlt  32099  fdvneggt  32100  fdvposle  32101  fdvnegge  32102  logdivsqrle  32150  bnj1253  32518  cvmlift2lem6  32787  satfun  32890  mrsubrn  32992  elmrsubrn  32999  elmsubrn  33007  msubrn  33008  onelssex  33180  trpredtr  33317  madebday  33638  imagesset  33805  ivthALT  34074  fness  34088  fneref  34089  refssfne  34097  fnemeet1  34105  fnejoin2  34108  filnetlem2  34118  filnetlem4  34120  ontgval  34170  knoppcnlem10  34232  knoppcnlem11  34233  bj-rabtr  34654  bj-rabtrAUTO  34656  bj-disj2r  34746  bj-restsnid  34783  bj-resta  34792  bj-imdirco  34886  elxp8  35069  finorwe  35080  mblfinlem3  35377  mblfinlem4  35378  ismblfin  35379  ovoliunnfl  35380  voliunnfl  35382  volsupnfl  35383  mbfposadd  35385  ftc1cnnclem  35409  ftc1cnnc  35410  ftc1anc  35419  ftc2nc  35420  areacirclem2  35427  areacirclem4  35429  areacirc  35431  caures  35479  constcncf  35481  brssrid  36183  brcnvssrid  36188  refrelid  36202  n0eldmqs  36324  atpsubN  37330  pol1N  37487  dia2dimlem13  38653  dibord  38736  dochvalr  38934  hdmapevec  39412  lcmineqlem10  39606  lcmineqlem12  39608  ismrcd1  40013  ismrc  40016  incssnn0  40026  mzpclall  40042  rmydioph  40329  rmxdioph  40331  expdiophlem2  40337  expdioph  40338  aomclem6  40377  kelac1  40381  gicabl  40417  arearect  40539  areaquad  40540  clcnvlem  40697  cnvtrcl0  40700  fvilbd  40764  relexp0a  40791  corcltrcl  40814  clsk1indlem2  41119  ntrclskb  41146  wnefimgd  41239  mnuprdlem4  41357  nzss  41395  lhe4.4ex1a  41407  dvsconst  41408  dvsid  41409  dvsef  41410  binomcxplemnn0  41427  onfrALTlem3  41624  onfrALTlem3VD  41967  unisn0  42062  founiiun0  42188  evthiccabs  42500  climconstmpt  42667  cncfshift  42883  addccncf2  42885  cncfcompt  42892  ioccncflimc  42894  icocncflimc  42898  cncfiooicclem1  42902  cncfiooicc  42903  cncfiooiccre  42904  cxpcncf2  42908  add1cncf  42910  add2cncf  42911  sub1cncfd  42912  sub2cncfd  42913  dvcosre  42921  dvmptfprod  42954  ibliooicc  42980  itgsincmulx  42983  itgsubsticclem  42984  itgiccshift  42989  itgperiod  42990  itgsbtaddcnst  42991  dirkeritg  43111  dirkercncflem2  43113  dirkercncflem4  43115  fourierdlem16  43132  fourierdlem18  43134  fourierdlem21  43137  fourierdlem22  43138  fourierdlem23  43139  fourierdlem32  43148  fourierdlem33  43149  fourierdlem39  43155  fourierdlem40  43156  fourierdlem57  43172  fourierdlem58  43173  fourierdlem59  43174  fourierdlem62  43177  fourierdlem68  43183  fourierdlem72  43187  fourierdlem73  43188  fourierdlem74  43189  fourierdlem75  43190  fourierdlem76  43191  fourierdlem78  43193  fourierdlem83  43198  fourierdlem84  43199  fourierdlem85  43200  fourierdlem88  43203  fourierdlem93  43208  fourierdlem94  43209  fourierdlem95  43210  fourierdlem97  43212  fourierdlem101  43216  fourierdlem103  43218  fourierdlem104  43219  fourierdlem111  43226  fourierdlem112  43227  fourierdlem113  43228  sqwvfoura  43237  sqwvfourb  43238  fouriersw  43240  fouriercn  43241  etransclem18  43261  etransclem22  43265  etransclem34  43277  etransclem46  43289  etransclem47  43290  sge0fsum  43393  meaiininclem  43492  hoidmvlelem2  43602  hspdifhsp  43622  hspmbllem2  43633  hspmbl  43635  iinhoiicclem  43679  pimgtmnf2  43716  smflimsuplem1  43818  smflimsuplem6  43823  srhmsubc  45068  srhmsubcALTV  45086