Theorem ssid 3875

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

Syntax hints:   ∈ wcel 2048   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839

This theorem is referenced by:  ssidd  3876  eqimssi  3911  eqimss2i  3912  nsspssun  4116  difid  4211  inv1  4228  disjpss  4287  pwidg  4431  elssuni  4735  unimax  4741  intmin  4763  rintn0  4890  sseliALT  5064  inxpssres  5417  xpss1  5419  xpss2  5420  residm  5725  resdm  5736  resmpt3  5745  ordunidif  6071  funresfunco  6223  dffn3  6349  fdmrn  6361  fvreseq1  6628  fimacnv  6658  iunpw  7303  onsucuni  7353  tfisi  7383  fparlem3  7610  fparlem4  7611  funsssuppss  7652  tfrlem1  7809  tz7.48-2  7874  oaordi  7965  omwordi  7990  omass  7999  nnaordi  8037  nnmwordi  8054  fpmg  8224  boxcutc  8294  domss2  8464  0fin  8533  en1eqsn  8535  findcard2d  8547  fimax2g  8551  domunfican  8578  pwfi  8606  fipreima  8617  fimin2g  8748  wofib  8796  wemapso  8802  noinfep  8909  cantnfval2  8918  tcidm  8974  tc0  8975  r1rankidb  9019  r1pw  9060  rankr1id  9077  scott0  9101  xpomen  9227  infpwfien  9274  alephsmo  9314  dfac12lem3  9357  cflem  9458  cflecard  9465  cfslb  9478  fin4en1  9521  fin23lem13  9544  fin23lem36  9560  isf32lem1  9565  fin67  9607  dcomex  9659  zorn2lem4  9711  alephexp2  9793  fpwwe2lem13  9854  canthnumlem  9860  wuncidm  9958  eltsk2g  9963  axgroth6  10040  axgroth3  10043  xrsup  13044  expcl  13255  hashcard  13524  hashf1lem2  13617  xptrrel  14191  cotrtrclfv  14223  rtrclreclem1  14268  lo1eq  14776  rlimeq  14777  serclim0  14785  isercolllem2  14873  isercoll  14875  fsum2d  14976  fsumabs  15006  fsumrlim  15016  fsumo1  15017  fsumiun  15026  fprod2d  15185  risefaccl  15219  fallfaccl  15220  eflt  15320  rpnnen2lem3  15419  rpnnen2lem5  15421  rpnnen2lem12  15428  rexpen  15431  ressid  16405  ressinbas  16406  oduclatb  17602  ipopos  17618  fpwipodrs  17622  ghmghmrn  18138  cntrnsg  18233  sylow3lem5  18507  lsmss1  18540  lsmss2  18542  gsumzres  18773  gsumzcl2  18774  gsumzf1o  18776  gsumadd  18786  gsumzmhm  18800  gsumzoppg  18807  dprdf1  18895  ablfac1eulem  18934  subrgid  19250  lbsextlem1  19642  rlmval2  19678  psrass1lem  19861  znf1o  20390  zntoslem  20395  css0  20525  uvcresum  20629  frlmlbs  20633  mdetrsca2  20907  mdetrlin2  20910  mdetunilem5  20919  mdetunilem9  20923  smadiadetglem1  20974  smadiadetglem2  20975  pmatcollpw3  21086  topopn  21208  fiinbas  21254  topbas  21274  topcld  21337  ntrtop  21372  opnneissb  21416  opnssneib  21417  opnneiid  21428  maxlp  21449  isperf2  21454  restperf  21486  idcn  21559  cnconst2  21585  lmres  21602  fiuncmp  21706  1stcelcls  21763  ssref  21814  refref  21815  kgencn2  21859  ptpjpre1  21873  ptbasfi  21883  xkopt  21957  elqtop2  22003  ptcmpfi  22115  fbssfi  22139  opnfbas  22144  filtop  22157  isfil2  22158  isfild  22160  fsubbas  22169  ssfg  22174  filssufilg  22213  ufileu  22221  imaelfm  22253  rnelfm  22255  fmfnfmlem4  22259  neiflim  22276  fclscf  22327  flimfnfcls  22330  tsmsfbas  22429  xpsxmet  22683  xpsdsval  22684  xpsmet  22685  tmsxms  22789  tmsms  22790  imasf1oxms  22792  imasf1oms  22793  prdsxms  22833  prdsms  22834  tmsxpsval  22841  retopbas  23062  cnngp  23081  cnopn  23088  cnperf  23121  retopconn  23130  fsumcn  23171  abscncf  23202  recncf  23203  imcncf  23204  cjcncf  23205  mulc1cncf  23206  cncfcn1  23211  cncfmpt2f  23215  cncfmpt2ss  23216  addccncf  23217  cdivcncf  23218  negcncf  23219  negfcncf  23220  abscncfALT  23221  cnmpopc  23225  xrhmeo  23243  oprpiece1res1  23248  oprpiece1res2  23249  cnrehmeo  23250  iscau3  23574  caubl  23604  caublcls  23605  evthicc2  23754  ovolre  23819  volsuplem  23849  uniiccdif  23872  uniioovol  23873  uniiccvol  23874  uniioombllem3  23879  uniioombllem4  23880  uniioombllem5  23881  dyadmbllem  23893  volivth  23901  itgfsum  24120  iblabslem  24121  iblabs  24122  bddmulibl  24132  cnlimc  24179  cnlimci  24180  dvcnp2  24210  dvcn  24211  cpnord  24225  cpnres  24227  dvmptntr  24261  dvmptfsum  24265  rolle  24280  dvlipcn  24284  c1liplem1  24286  dvivth  24300  dvfsumabs  24313  ftc1a  24327  ftc1cn  24333  plyssc  24483  plyeq0  24494  0dgr  24528  coemulc  24538  coe0  24539  coesub  24540  coe1termlem  24541  dgrmulc  24554  dgrsub  24555  dvnply2  24569  plycpn  24571  plyremlem  24586  fta1lem  24589  vieta1lem2  24593  aalioulem3  24616  taylthlem1  24654  taylthlem2  24655  ulmcn  24680  psercn  24707  abelth  24722  efcn  24724  efcvx  24730  dvrelog  24911  logcn  24921  dvloglem  24922  dvlog  24925  dvlog2  24927  efopnlem2  24931  logccv  24937  cxpcn  25017  cxpcn3  25020  resqrtcn  25021  sqrtcn  25022  loglesqrt  25030  atancn  25205  jensen  25258  ftalem3  25344  dchrfi  25523  dchrisumlema  25756  pntlem3  25877  uhgrsubgrself  26755  uhgrspansubgr  26766  umgr2adedgwlk  27441  umgr2adedgwlkon  27442  umgr2adedgspth  27444  upgr1wlkdlem2  27665  sspid  28269  ssps  28274  helch  28789  hhssnv  28810  hhsssh  28815  shintcl  28878  chintcl  28880  shlesb1i  28934  omlsi  28952  chlejb1i  29024  chm0i  29038  chabs1  29064  chabs2  29065  spanun  29093  cmidi  29158  pjidmcoi  29725  csmdsymi  29882  sumdmdlem2  29967  dmdbr5ati  29970  mdcompli  29977  dmdcompli  29978  disjdifprg  30081  fcoinver  30111  f1rnen  30127  xppreima  30146  padct  30196  xrinfm  30219  clatp0cl  30368  clatp1cl  30369  xrsp0  30378  xrsp1  30379  gsumle  30478  gsumvsca1  30481  gsumvsca2  30482  cntrcmnd  30489  cntrabl  30490  cntrcrng  30491  ellspds  30562  reff  30704  locfinreflem  30705  esumsnf  30924  esumcvg  30946  sigagenid  31012  iblidicc  31472  cxpcncf1  31475  fdvposlt  31479  fdvneggt  31480  fdvposle  31481  fdvnegge  31482  logdivsqrle  31530  bnj1253  31895  cvmlift2lem6  32100  mrsubrn  32220  elmrsubrn  32227  elmsubrn  32235  msubrn  32236  trpredtr  32530  imagesset  32875  ivthALT  33144  fness  33158  fneref  33159  refssfne  33167  fnemeet1  33175  fnejoin2  33178  filnetlem2  33188  filnetlem4  33190  ontgval  33239  knoppcnlem10  33301  knoppcnlem11  33302  bj-rabtr  33683  bj-rabtrAUTO  33685  bj-disj2r  33790  bj-restsnid  33823  bj-resta  33832  elxp8  34029  mblfinlem3  34320  mblfinlem4  34321  ismblfin  34322  ovoliunnfl  34323  voliunnfl  34325  volsupnfl  34326  mbfposadd  34328  ftc1cnnclem  34354  ftc1cnnc  34355  ftc1anc  34364  ftc2nc  34365  areacirclem2  34372  areacirclem4  34374  areacirc  34376  caures  34425  constcncf  34427  idcncf  34428  sub1cncf  34429  sub2cncf  34430  brssrid  35135  brcnvssrid  35140  refrelid  35154  n0eldmqs  35276  atpsubN  36282  pol1N  36439  dia2dimlem13  37605  dibord  37688  dochvalr  37886  hdmapevec  38364  ismrcd1  38635  ismrc  38638  incssnn0  38648  mzpclall  38664  rmydioph  38952  rmxdioph  38954  expdiophlem2  38960  expdioph  38961  aomclem6  39000  kelac1  39004  gicabl  39040  arearect  39163  areaquad  39164  clcnvlem  39291  cnvtrcl0  39294  fvilbd  39342  relexp0a  39369  corcltrcl  39392  clsk1indlem2  39700  ntrclskb  39727  wnefimgd  39820  mnuprdlem4  39931  nzss  40009  lhe4.4ex1a  40021  dvsconst  40022  dvsid  40023  dvsef  40024  binomcxplemnn0  40041  onfrALTlem3  40241  onfrALTlem3VD  40584  unisn0  40680  founiiun0  40821  evthiccabs  41148  climconstmpt  41316  cncfshift  41533  addccncf2  41535  cncfcompt  41542  ioccncflimc  41544  icocncflimc  41548  cncfiooicclem1  41552  cncfiooicc  41553  cncfiooiccre  41554  cxpcncf2  41559  add1cncf  41561  add2cncf  41562  sub1cncfd  41563  sub2cncfd  41564  dvcosre  41572  dvmptfprod  41606  ibliooicc  41632  itgsincmulx  41635  itgsubsticclem  41636  itgiccshift  41641  itgperiod  41642  itgsbtaddcnst  41643  dirkeritg  41764  dirkercncflem2  41766  dirkercncflem4  41768  fourierdlem16  41785  fourierdlem18  41787  fourierdlem21  41790  fourierdlem22  41791  fourierdlem23  41792  fourierdlem32  41801  fourierdlem33  41802  fourierdlem39  41808  fourierdlem40  41809  fourierdlem57  41825  fourierdlem58  41826  fourierdlem59  41827  fourierdlem62  41830  fourierdlem68  41836  fourierdlem72  41840  fourierdlem73  41841  fourierdlem74  41842  fourierdlem75  41843  fourierdlem76  41844  fourierdlem78  41846  fourierdlem83  41851  fourierdlem84  41852  fourierdlem85  41853  fourierdlem88  41856  fourierdlem93  41861  fourierdlem94  41862  fourierdlem95  41863  fourierdlem97  41865  fourierdlem101  41869  fourierdlem103  41871  fourierdlem104  41872  fourierdlem111  41879  fourierdlem112  41880  fourierdlem113  41881  sqwvfoura  41890  sqwvfourb  41891  fouriersw  41893  fouriercn  41894  etransclem18  41914  etransclem22  41918  etransclem34  41930  etransclem46  41942  etransclem47  41943  sge0fsum  42046  meaiininclem  42145  hoidmvlelem2  42255  hspdifhsp  42275  hspmbllem2  42286  hspmbl  42288  iinhoiicclem  42332  pimgtmnf2  42369  smflimsuplem1  42471  smflimsuplem6  42476  srhmsubc  43651  srhmsubcALTV  43669