Theorem ssid 3966

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927

This theorem is referenced by:  ssidd  3967  eqimssi  4002  eqimss2i  4003  nsspssun  4217  difidALT  4331  inv1  4354  disjpss  4420  pwidg  4580  elssuni  4898  unimax  4905  intmin  4929  rintn0  5069  sseliALT  5266  inxpssres  5650  xpss1  5652  xpss2  5653  residm  5970  resdm  5982  resmpt3  5992  cnvrescnv  6147  onelssex  6365  ordunidif  6366  funresfunco  6542  dffn3  6681  fdmrn  6700  fvreseq1  6989  fimacnvOLD  7021  iunpw  7705  onsucuni  7763  tfisi  7795  fparlem3  8046  fparlem4  8047  funsssuppss  8121  tfrlem1  8322  tz7.48-2  8388  oaordi  8493  omwordi  8518  omass  8527  nnaordi  8565  nnmwordi  8582  naddunif  8637  fpmg  8806  boxcutc  8879  domss2  9080  findcard2d  9110  0fin  9115  en1eqsnOLD  9219  fimax2g  9233  domunfican  9264  pwfiOLD  9291  fipreima  9302  fimin2g  9433  wofib  9481  wemapso  9487  noinfep  9596  cantnfval2  9605  tcidm  9682  tc0  9683  r1rankidb  9740  r1pw  9781  rankr1id  9798  scott0  9822  xpomen  9951  infpwfien  9998  alephsmo  10038  dfac12lem3  10081  cflem  10182  cflecard  10189  cfslb  10202  fin4en1  10245  fin23lem13  10268  fin23lem36  10284  isf32lem1  10289  fin67  10331  dcomex  10383  zorn2lem4  10435  alephexp2  10517  fpwwe2lem12  10578  canthnumlem  10584  wuncidm  10682  eltsk2g  10687  axgroth6  10764  axgroth3  10767  xrsup  13773  expcl  13985  hashcard  14255  hashf1lem2  14355  xptrrel  14865  cotrtrclfv  14897  rtrclreclem2  14944  lo1eq  15450  rlimeq  15451  serclim0  15459  isercolllem2  15550  isercoll  15552  fsum2d  15656  fsumabs  15686  fsumrlim  15696  fsumo1  15697  fsumiun  15706  fprod2d  15864  risefaccl  15898  fallfaccl  15899  eflt  15999  rpnnen2lem3  16098  rpnnen2lem5  16100  rpnnen2lem12  16107  rexpen  16110  ressid  17125  ressinbas  17126  oduclatb  18396  ipopos  18425  fpwipodrs  18429  ghmghmrn  19027  cntrnsg  19122  0symgefmndeq  19175  sylow3lem5  19413  lsmss1  19447  lsmss2  19449  cntrcmnd  19620  cntrabl  19621  gsumzres  19686  gsumzcl2  19687  gsumzf1o  19689  gsumadd  19700  gsumzmhm  19714  gsumzoppg  19721  dprdf1  19812  ablfac1eulem  19851  subrgid  20224  lbsextlem1  20619  rlmval2  20663  znf1o  20958  zntoslem  20963  css0  21093  uvcresum  21199  frlmlbs  21203  psrass1lemOLD  21342  psrass1lem  21345  mdetrsca2  21953  mdetrlin2  21956  mdetunilem5  21965  mdetunilem9  21969  smadiadetglem1  22020  smadiadetglem2  22021  pmatcollpw3  22133  topopn  22255  fiinbas  22302  topbas  22322  topcld  22386  ntrtop  22421  opnneissb  22465  opnssneib  22466  opnneiid  22477  maxlp  22498  isperf2  22503  restperf  22535  idcn  22608  cnconst2  22634  lmres  22651  fiuncmp  22755  1stcelcls  22812  ssref  22863  refref  22864  kgencn2  22908  ptpjpre1  22922  ptbasfi  22932  xkopt  23006  elqtop2  23052  ptcmpfi  23164  fbssfi  23188  opnfbas  23193  filtop  23206  isfil2  23207  isfild  23209  fsubbas  23218  ssfg  23223  filssufilg  23262  ufileu  23270  imaelfm  23302  rnelfm  23304  fmfnfmlem4  23308  neiflim  23325  fclscf  23376  flimfnfcls  23379  tsmsfbas  23479  xpsxmet  23733  xpsdsval  23734  xpsmet  23735  tmsxms  23842  tmsms  23843  imasf1oxms  23845  imasf1oms  23846  prdsxms  23886  prdsms  23887  tmsxpsval  23894  retopbas  24124  cnngp  24143  cnopn  24150  cnperf  24183  retopconn  24192  fsumcn  24233  abscncf  24264  recncf  24265  imcncf  24266  cjcncf  24267  mulc1cncf  24268  cncfcn1  24274  cncfmpt2f  24278  cncfmpt2ss  24279  addccncf  24280  idcncf  24281  sub1cncf  24282  sub2cncf  24283  cdivcncf  24284  negcncf  24285  negfcncf  24286  abscncfALT  24287  cnmpopc  24291  xrhmeo  24309  oprpiece1res1  24314  oprpiece1res2  24315  cnrehmeo  24316  iscau3  24642  caubl  24672  caublcls  24673  evthicc2  24824  ovolre  24889  volsuplem  24919  uniiccdif  24942  uniioovol  24943  uniiccvol  24944  uniioombllem3  24949  uniioombllem4  24950  uniioombllem5  24951  dyadmbllem  24963  volivth  24971  itgfsum  25191  iblabslem  25192  iblabs  25193  bddmulibl  25203  cnlimc  25252  cnlimci  25253  dvcnp2  25284  dvcn  25285  cpnord  25299  cpnres  25301  dvmptntr  25335  dvmptfsum  25339  rolle  25354  dvlipcn  25358  c1liplem1  25360  dvivth  25374  dvfsumabs  25387  ftc1a  25401  ftc1cn  25407  plyssc  25561  plyeq0  25572  0dgr  25606  coemulc  25616  coe0  25617  coesub  25618  coe1termlem  25619  dgrmulc  25632  dgrsub  25633  dvnply2  25647  plycpn  25649  plyremlem  25664  fta1lem  25667  vieta1lem2  25671  aalioulem3  25694  taylthlem1  25732  taylthlem2  25733  ulmcn  25758  psercn  25785  abelth  25800  efcn  25802  efcvx  25808  dvrelog  25992  logcn  26002  dvloglem  26003  dvlog  26006  dvlog2  26008  efopnlem2  26012  logccv  26018  cxpcn  26098  cxpcn3  26101  resqrtcn  26102  sqrtcn  26103  loglesqrt  26111  atancn  26286  jensen  26338  ftalem3  26424  dchrfi  26603  dchrisumlema  26836  pntlem3  26957  madebday  27229  uhgrsubgrself  28228  uhgrspansubgr  28239  umgr2adedgwlk  28890  umgr2adedgwlkon  28891  umgr2adedgspth  28893  upgr1wlkdlem2  29090  sspid  29667  ssps  29672  helch  30185  hhssnv  30206  hhsssh  30211  shintcl  30272  chintcl  30274  shlesb1i  30328  omlsi  30346  chlejb1i  30418  chm0i  30432  chabs1  30458  chabs2  30459  spanun  30487  cmidi  30552  pjidmcoi  31119  csmdsymi  31276  sumdmdlem2  31361  dmdbr5ati  31364  mdcompli  31371  dmdcompli  31372  disjdifprg  31493  fcoinver  31525  f1rnen  31543  xppreima  31562  padct  31636  xrinfm  31659  clatp0cl  31836  clatp1cl  31837  xrsp0  31872  xrsp1  31873  cntrcrng  31904  gsumle  31932  cycpmconjslem1  32003  cycpmconjslem2  32004  gsumvsca1  32061  gsumvsca2  32062  qusxpid  32151  ellspds  32157  rspidlid  32163  reff  32420  locfinreflem  32421  esumsnf  32663  esumcvg  32685  sigagenid  32750  iblidicc  33205  cxpcncf1  33208  fdvposlt  33212  fdvneggt  33213  fdvposle  33214  fdvnegge  33215  logdivsqrle  33263  bnj1253  33629  fineqvac  33698  cvmlift2lem6  33902  satfun  34005  mrsubrn  34107  elmrsubrn  34114  elmsubrn  34122  msubrn  34123  imagesset  34538  ivthALT  34807  fness  34821  fneref  34822  refssfne  34830  fnemeet1  34838  fnejoin2  34841  filnetlem2  34851  filnetlem4  34853  ontgval  34903  knoppcnlem10  34965  knoppcnlem11  34966  bj-rabtr  35400  bj-rabtrAUTO  35402  bj-disj2r  35499  bj-restsnid  35558  bj-resta  35567  bj-imdirco  35661  elxp8  35842  finorwe  35853  mblfinlem3  36117  mblfinlem4  36118  ismblfin  36119  ovoliunnfl  36120  voliunnfl  36122  volsupnfl  36123  mbfposadd  36125  ftc1cnnclem  36149  ftc1cnnc  36150  ftc1anc  36159  ftc2nc  36160  areacirclem2  36167  areacirclem4  36169  areacirc  36171  caures  36219  constcncf  36221  brssrid  36964  brcnvssrid  36969  refrelid  36984  n0eldmqs  37110  atpsubN  38216  pol1N  38373  dia2dimlem13  39539  dibord  39622  dochvalr  39820  hdmapevec  40298  lcmineqlem10  40495  lcmineqlem12  40497  eqimssd  40635  ressbasssg  40668  ismrcd1  41007  ismrc  41010  incssnn0  41020  mzpclall  41036  rmydioph  41324  rmxdioph  41326  expdiophlem2  41332  expdioph  41333  aomclem6  41372  kelac1  41376  gicabl  41412  arearect  41535  areaquad  41536  unielid  41539  oege2  41627  oacl2g  41650  ofoaf  41655  clcnvlem  41885  cnvtrcl0  41888  fvilbd  41951  relexp0a  41978  corcltrcl  42001  clsk1indlem2  42304  ntrclskb  42331  wnefimgd  42424  mnuprdlem4  42545  nzss  42587  lhe4.4ex1a  42599  dvsconst  42600  dvsid  42601  dvsef  42602  binomcxplemnn0  42619  onfrALTlem3  42816  onfrALTlem3VD  43159  unisn0  43252  founiiun0  43399  evthiccabs  43724  climconstmpt  43889  cncfshift  44105  addccncf2  44107  cncfcompt  44114  ioccncflimc  44116  icocncflimc  44120  cncfiooicclem1  44124  cncfiooicc  44125  cncfiooiccre  44126  cxpcncf2  44130  add1cncf  44132  add2cncf  44133  sub1cncfd  44134  sub2cncfd  44135  dvcosre  44143  dvmptfprod  44176  ibliooicc  44202  itgsincmulx  44205  itgsubsticclem  44206  itgiccshift  44211  itgperiod  44212  itgsbtaddcnst  44213  dirkeritg  44333  dirkercncflem2  44335  dirkercncflem4  44337  fourierdlem16  44354  fourierdlem18  44356  fourierdlem21  44359  fourierdlem22  44360  fourierdlem23  44361  fourierdlem32  44370  fourierdlem33  44371  fourierdlem39  44377  fourierdlem40  44378  fourierdlem57  44394  fourierdlem58  44395  fourierdlem59  44396  fourierdlem62  44399  fourierdlem68  44405  fourierdlem72  44409  fourierdlem73  44410  fourierdlem74  44411  fourierdlem75  44412  fourierdlem76  44413  fourierdlem78  44415  fourierdlem83  44420  fourierdlem84  44421  fourierdlem85  44422  fourierdlem88  44425  fourierdlem93  44430  fourierdlem94  44431  fourierdlem95  44432  fourierdlem97  44434  fourierdlem101  44438  fourierdlem103  44440  fourierdlem104  44441  fourierdlem111  44448  fourierdlem112  44449  fourierdlem113  44450  sqwvfoura  44459  sqwvfourb  44460  fouriersw  44462  fouriercn  44463  etransclem18  44483  etransclem22  44487  etransclem34  44499  etransclem46  44511  etransclem47  44512  sge0fsum  44618  meaiininclem  44717  hoidmvlelem2  44827  hspdifhsp  44847  hspmbllem2  44858  hspmbl  44860  iinhoiicclem  44904  pimgtmnf2  44945  smflimsuplem1  45051  smflimsuplem6  45056  srhmsubc  46364  srhmsubcALTV  46382