Theorem ssid 3953

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898

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

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

This theorem is referenced by:  ssidd  3954  eqimssd  3987  eqimsscd  3988  eqimssi  3991  eqimss2i  3992  nsspssun  4217  difidALT  4326  inv1  4347  disjpss  4410  pwidg  4569  elssuni  4889  unimax  4895  intmin  4918  rintn0  5059  sseliALT  5249  inxpssres  5636  xpss1  5638  xpss2  5639  residm  5963  resdm  5979  resmpt3  5991  cnvrescnv  6147  onelssex  6360  ordunidif  6361  funresfunco  6527  dffn3  6668  fdmrn  6687  fvreseq1  6978  iunpw  7710  onsucuni  7764  tfisi  7795  fparlem3  8050  fparlem4  8051  funsssuppss  8126  tfrlem1  8301  tz7.48-2  8367  oaordi  8467  omwordi  8492  omass  8501  nnaordi  8539  nnmwordi  8556  naddunif  8614  fpmg  8798  boxcutc  8871  domss2  9056  findcard2d  9083  fimax2g  9177  domunfican  9213  fipreima  9249  fimin2g  9390  wofib  9438  wemapso  9444  noinfep  9557  cantnfval2  9566  tcidm  9641  tc0  9642  r1rankidb  9704  r1pw  9745  rankr1id  9762  scott0  9786  xpomen  9913  infpwfien  9960  alephsmo  10000  dfac12lem3  10044  cflem  10143  cflemOLD  10144  cflecard  10151  cfslb  10164  fin4en1  10207  fin23lem13  10230  fin23lem36  10246  isf32lem1  10251  fin67  10293  dcomex  10345  zorn2lem4  10397  alephexp2  10479  fpwwe2lem12  10540  canthnumlem  10546  wuncidm  10644  eltsk2g  10649  axgroth6  10726  axgroth3  10729  xrsup  13774  expcl  13988  hashcard  14264  hashf1lem2  14365  xptrrel  14889  cotrtrclfv  14921  rtrclreclem2  14968  lo1eq  15477  rlimeq  15478  serclim0  15486  isercolllem2  15575  isercoll  15577  fsum2d  15680  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  fprod2d  15890  risefaccl  15924  fallfaccl  15925  eflt  16028  rpnnen2lem3  16127  rpnnen2lem5  16129  rpnnen2lem12  16136  rexpen  16139  ressbasssg  17150  ressid  17157  ressinbas  17158  oduclatb  18415  ipopos  18444  fpwipodrs  18448  ghmghmrn  19149  elcntr  19244  cntrnsg  19258  0symgefmndeq  19308  sylow3lem5  19545  lsmss1  19579  lsmss2  19581  cmnbascntr  19719  cntrcmnd  19756  cntrabl  19757  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumadd  19837  gsumzmhm  19851  gsumzoppg  19858  dprdf1  19949  ablfac1eulem  19988  gsumle  20059  subrgid  20490  srhmsubc  20597  lbsextlem1  21097  rlmval2  21128  znf1o  21490  zntoslem  21495  css0  21628  uvcresum  21732  frlmlbs  21736  psrass1lem  21871  mdetrsca2  22520  mdetrlin2  22523  mdetunilem5  22532  mdetunilem9  22536  smadiadetglem1  22587  smadiadetglem2  22588  pmatcollpw3  22700  topopn  22822  fiinbas  22868  topbas  22888  topcld  22951  ntrtop  22986  opnneissb  23030  opnssneib  23031  opnneiid  23042  maxlp  23063  isperf2  23068  restperf  23100  idcn  23173  cnconst2  23199  lmres  23216  fiuncmp  23320  1stcelcls  23377  ssref  23428  refref  23429  kgencn2  23473  ptpjpre1  23487  ptbasfi  23497  xkopt  23571  elqtop2  23617  ptcmpfi  23729  fbssfi  23753  opnfbas  23758  filtop  23771  isfil2  23772  isfild  23774  fsubbas  23783  ssfg  23788  filssufilg  23827  ufileu  23835  imaelfm  23867  rnelfm  23869  fmfnfmlem4  23873  neiflim  23890  fclscf  23941  flimfnfcls  23944  tsmsfbas  24044  xpsxmet  24296  xpsdsval  24297  xpsmet  24298  tmsxms  24402  tmsms  24403  imasf1oxms  24405  imasf1oms  24406  prdsxms  24446  prdsms  24447  tmsxpsval  24454  retopbas  24676  cnngp  24695  cnopn  24702  cnperf  24737  retopconn  24746  fsumcn  24789  abscncf  24822  recncf  24823  imcncf  24824  cjcncf  24825  mulc1cncf  24826  cncfcn1  24832  cncfmpt2f  24836  cncfmpt2ss  24837  addccncf  24838  idcncf  24839  sub1cncf  24840  sub2cncf  24841  cdivcncf  24842  negcncf  24843  negcncfOLD  24844  negfcncf  24845  abscncfALT  24846  cnmpopc  24850  xrhmeo  24872  oprpiece1res1  24877  oprpiece1res2  24878  cnrehmeo  24879  cnrehmeoOLD  24880  iscau3  25206  caubl  25236  caublcls  25237  mulcncf  25374  evthicc2  25389  ovolre  25454  volsuplem  25484  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  dyadmbllem  25528  volivth  25536  itgfsum  25756  iblabslem  25757  iblabs  25758  bddmulibl  25768  cnlimc  25817  cnlimci  25818  dvcnp2  25849  dvcnp2OLD  25850  dvcn  25851  cpnord  25865  cpnres  25867  dvmptntr  25903  dvmptfsum  25907  rolle  25922  dvlipcn  25927  c1liplem1  25929  dvivth  25943  dvfsumabs  25957  ftc1a  25972  ftc1cn  25978  plyssc  26133  plyeq0  26144  0dgr  26178  coemulc  26188  coe0  26189  coesub  26190  coe1termlem  26191  dgrmulc  26205  dgrsub  26206  dvnply2  26223  plycpn  26225  plyremlem  26240  fta1lem  26243  vieta1lem2  26247  aalioulem3  26270  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmcn  26336  psercn  26364  abelth  26379  efcn  26381  efcvx  26387  dvrelog  26574  logcn  26584  dvloglem  26585  dvlog  26588  dvlog2  26590  efopnlem2  26594  logccv  26600  cxpcn  26682  cxpcnOLD  26683  cxpcn3  26686  resqrtcn  26687  sqrtcn  26688  loglesqrt  26699  atancn  26874  jensen  26927  ftalem3  27013  dchrfi  27194  dchrisumlema  27427  pntlem3  27548  madebday  27846  expscl  28355  uhgrsubgrself  29260  uhgrspansubgr  29271  umgr2adedgwlk  29925  umgr2adedgwlkon  29926  umgr2adedgspth  29928  upgr1wlkdlem2  30128  sspid  30707  ssps  30712  helch  31225  hhssnv  31246  hhsssh  31251  shintcl  31312  chintcl  31314  shlesb1i  31368  omlsi  31386  chlejb1i  31458  chm0i  31472  chabs1  31498  chabs2  31499  spanun  31527  cmidi  31592  pjidmcoi  32159  csmdsymi  32316  sumdmdlem2  32401  dmdbr5ati  32404  mdcompli  32411  dmdcompli  32412  disjdifprg  32557  fcoinver  32586  f1rnen  32612  xppreima  32629  padct  32705  xrinfm  32742  indconst1  32847  clatp0cl  32964  clatp1cl  32965  xrsp0  33000  xrsp1  33001  cntrcrng  33057  cycpmconjslem1  33130  cycpmconjslem2  33131  gsumvsca1  33202  gsumvsca2  33203  qusxpid  33335  ellspds  33340  rspidlid  33347  rlmdim  33643  reff  33873  locfinreflem  33874  esumsnf  34098  esumcvg  34120  sigagenid  34185  iblidicc  34626  cxpcncf1  34629  fdvposlt  34633  fdvneggt  34634  fdvposle  34635  fdvnegge  34636  logdivsqrle  34684  bnj1253  35050  fineqvac  35160  fineqvnttrclse  35165  cvmlift2lem6  35373  satfun  35476  mrsubrn  35578  elmrsubrn  35585  elmsubrn  35593  msubrn  35594  imagesset  36018  ivthALT  36400  fness  36414  fneref  36415  refssfne  36423  fnemeet1  36431  fnejoin2  36434  filnetlem2  36444  filnetlem4  36446  ontgval  36496  knoppcnlem10  36567  knoppcnlem11  36568  bj-rabtr  36995  bj-rabtrAUTO  36997  bj-disj2r  37093  bj-restsnid  37152  bj-resta  37161  bj-imdirco  37255  elxp8  37436  finorwe  37447  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  mbfposadd  37727  ftc1cnnclem  37751  ftc1cnnc  37752  ftc1anc  37761  ftc2nc  37762  areacirclem2  37769  areacirclem4  37771  areacirc  37773  caures  37820  constcncf  37822  brssrid  38614  brcnvssrid  38619  refrelid  38634  n0eldmqs  38765  atpsubN  39872  pol1N  40029  dia2dimlem13  41195  dibord  41278  dochvalr  41476  hdmapevec  41954  lcmineqlem10  42151  lcmineqlem12  42153  ismrcd1  42815  ismrc  42818  incssnn0  42828  mzpclall  42844  rmydioph  43131  rmxdioph  43133  expdiophlem2  43139  expdioph  43140  aomclem6  43176  kelac1  43180  gicabl  43216  arearect  43332  areaquad  43333  unielid  43336  oege2  43424  oacl2g  43447  ofoaf  43472  clcnvlem  43740  cnvtrcl0  43743  fvilbd  43806  relexp0a  43833  corcltrcl  43856  clsk1indlem2  44159  ntrclskb  44186  wnefimgd  44278  mnuprdlem4  44392  nzss  44434  lhe4.4ex1a  44446  dvsconst  44447  dvsid  44448  dvsef  44449  binomcxplemnn0  44466  onfrALTlem3  44661  onfrALTlem3VD  45003  unisn0  45175  founiiun0  45311  evthiccabs  45620  climconstmpt  45780  cncfshift  45996  addccncf2  45998  cncfcompt  46005  ioccncflimc  46007  icocncflimc  46011  cncfiooicclem1  46015  cncfiooicc  46016  cncfiooiccre  46017  cxpcncf2  46021  add1cncf  46023  add2cncf  46024  sub1cncfd  46025  sub2cncfd  46026  dvcosre  46034  dvmptfprod  46067  ibliooicc  46093  itgsincmulx  46096  itgsubsticclem  46097  itgiccshift  46102  itgperiod  46103  itgsbtaddcnst  46104  dirkeritg  46224  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem16  46245  fourierdlem18  46247  fourierdlem21  46250  fourierdlem22  46251  fourierdlem23  46252  fourierdlem32  46261  fourierdlem33  46262  fourierdlem39  46268  fourierdlem40  46269  fourierdlem57  46285  fourierdlem58  46286  fourierdlem59  46287  fourierdlem62  46290  fourierdlem68  46296  fourierdlem72  46300  fourierdlem73  46301  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem78  46306  fourierdlem83  46311  fourierdlem84  46312  fourierdlem85  46313  fourierdlem88  46316  fourierdlem93  46321  fourierdlem94  46322  fourierdlem95  46323  fourierdlem97  46325  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  fourierdlem113  46341  sqwvfoura  46350  sqwvfourb  46351  fouriersw  46353  fouriercn  46354  etransclem18  46374  etransclem22  46378  etransclem34  46390  etransclem46  46402  etransclem47  46403  sge0fsum  46509  meaiininclem  46608  hoidmvlelem2  46718  hspdifhsp  46738  hspmbllem2  46749  hspmbl  46751  iinhoiicclem  46795  pimgtmnf2  46836  smflimsuplem1  46942  smflimsuplem6  46947  cjnpoly  47013  srhmsubcALTV  48449  imaidfu2lem  49234  imaidfu  49235  imaidfu2  49236  setc1onsubc  49727