Theorem ssid 4031

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976

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

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

This theorem is referenced by:  ssidd  4032  eqimssd  4065  eqimsscd  4066  eqimssi  4069  eqimss2i  4070  nsspssun  4287  difidALT  4399  inv1  4421  disjpss  4484  pwidg  4642  elssuni  4961  unimax  4968  intmin  4992  rintn0  5132  sseliALT  5327  inxpssres  5717  xpss1  5719  xpss2  5720  residm  6039  resdm  6055  resmpt3  6067  cnvrescnv  6226  onelssex  6443  ordunidif  6444  funresfunco  6619  dffn3  6759  fdmrn  6779  fvreseq1  7072  fimacnvOLD  7104  iunpw  7806  onsucuni  7864  tfisi  7896  fparlem3  8155  fparlem4  8156  funsssuppss  8231  tfrlem1  8432  tz7.48-2  8498  oaordi  8602  omwordi  8627  omass  8636  nnaordi  8674  nnmwordi  8691  naddunif  8749  fpmg  8926  boxcutc  8999  domss2  9202  findcard2d  9232  0finOLD  9237  en1eqsnOLD  9337  fimax2g  9350  domunfican  9389  pwfiOLD  9417  fipreima  9428  fimin2g  9566  wofib  9614  wemapso  9620  noinfep  9729  cantnfval2  9738  tcidm  9815  tc0  9816  r1rankidb  9873  r1pw  9914  rankr1id  9931  scott0  9955  xpomen  10084  infpwfien  10131  alephsmo  10171  dfac12lem3  10215  cflem  10314  cflemOLD  10315  cflecard  10322  cfslb  10335  fin4en1  10378  fin23lem13  10401  fin23lem36  10417  isf32lem1  10422  fin67  10464  dcomex  10516  zorn2lem4  10568  alephexp2  10650  fpwwe2lem12  10711  canthnumlem  10717  wuncidm  10815  eltsk2g  10820  axgroth6  10897  axgroth3  10900  xrsup  13919  expcl  14130  hashcard  14404  hashf1lem2  14505  xptrrel  15029  cotrtrclfv  15061  rtrclreclem2  15108  lo1eq  15614  rlimeq  15615  serclim0  15623  isercolllem2  15714  isercoll  15716  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2d  16029  risefaccl  16063  fallfaccl  16064  eflt  16165  rpnnen2lem3  16264  rpnnen2lem5  16266  rpnnen2lem12  16273  rexpen  16276  ressbasssg  17295  ressid  17303  ressinbas  17304  oduclatb  18577  ipopos  18606  fpwipodrs  18610  ghmghmrn  19275  elcntr  19370  cntrnsg  19384  0symgefmndeq  19435  sylow3lem5  19673  lsmss1  19707  lsmss2  19709  cmnbascntr  19847  cntrcmnd  19884  cntrabl  19885  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumadd  19965  gsumzmhm  19979  gsumzoppg  19986  dprdf1  20077  ablfac1eulem  20116  subrgid  20601  srhmsubc  20702  lbsextlem1  21183  rlmval2  21222  znf1o  21593  zntoslem  21598  css0  21730  uvcresum  21836  frlmlbs  21840  psrass1lem  21975  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  mdetunilem9  22647  smadiadetglem1  22698  smadiadetglem2  22699  pmatcollpw3  22811  topopn  22933  fiinbas  22980  topbas  23000  topcld  23064  ntrtop  23099  opnneissb  23143  opnssneib  23144  opnneiid  23155  maxlp  23176  isperf2  23181  restperf  23213  idcn  23286  cnconst2  23312  lmres  23329  fiuncmp  23433  1stcelcls  23490  ssref  23541  refref  23542  kgencn2  23586  ptpjpre1  23600  ptbasfi  23610  xkopt  23684  elqtop2  23730  ptcmpfi  23842  fbssfi  23866  opnfbas  23871  filtop  23884  isfil2  23885  isfild  23887  fsubbas  23896  ssfg  23901  filssufilg  23940  ufileu  23948  imaelfm  23980  rnelfm  23982  fmfnfmlem4  23986  neiflim  24003  fclscf  24054  flimfnfcls  24057  tsmsfbas  24157  xpsxmet  24411  xpsdsval  24412  xpsmet  24413  tmsxms  24520  tmsms  24521  imasf1oxms  24523  imasf1oms  24524  prdsxms  24564  prdsms  24565  tmsxpsval  24572  retopbas  24802  cnngp  24821  cnopn  24828  cnperf  24861  retopconn  24870  fsumcn  24913  abscncf  24946  recncf  24947  imcncf  24948  cjcncf  24949  mulc1cncf  24950  cncfcn1  24956  cncfmpt2f  24960  cncfmpt2ss  24961  addccncf  24962  idcncf  24963  sub1cncf  24964  sub2cncf  24965  cdivcncf  24966  negcncf  24967  negcncfOLD  24968  negfcncf  24969  abscncfALT  24970  cnmpopc  24974  xrhmeo  24996  oprpiece1res1  25001  oprpiece1res2  25002  cnrehmeo  25003  cnrehmeoOLD  25004  iscau3  25331  caubl  25361  caublcls  25362  mulcncf  25499  evthicc2  25514  ovolre  25579  volsuplem  25609  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  dyadmbllem  25653  volivth  25661  itgfsum  25882  iblabslem  25883  iblabs  25884  bddmulibl  25894  cnlimc  25943  cnlimci  25944  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  cpnord  25991  cpnres  25993  dvmptntr  26029  dvmptfsum  26033  rolle  26048  dvlipcn  26053  c1liplem1  26055  dvivth  26069  dvfsumabs  26083  ftc1a  26098  ftc1cn  26104  plyssc  26259  plyeq0  26270  0dgr  26304  coemulc  26314  coe0  26315  coesub  26316  coe1termlem  26317  dgrmulc  26331  dgrsub  26332  dvnply2  26347  plycpn  26349  plyremlem  26364  fta1lem  26367  vieta1lem2  26371  aalioulem3  26394  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmcn  26460  psercn  26488  abelth  26503  efcn  26505  efcvx  26511  dvrelog  26697  logcn  26707  dvloglem  26708  dvlog  26711  dvlog2  26713  efopnlem2  26717  logccv  26723  cxpcn  26805  cxpcnOLD  26806  cxpcn3  26809  resqrtcn  26810  sqrtcn  26811  loglesqrt  26822  atancn  26997  jensen  27050  ftalem3  27136  dchrfi  27317  dchrisumlema  27550  pntlem3  27671  madebday  27956  uhgrsubgrself  29315  uhgrspansubgr  29326  umgr2adedgwlk  29978  umgr2adedgwlkon  29979  umgr2adedgspth  29981  upgr1wlkdlem2  30178  sspid  30757  ssps  30762  helch  31275  hhssnv  31296  hhsssh  31301  shintcl  31362  chintcl  31364  shlesb1i  31418  omlsi  31436  chlejb1i  31508  chm0i  31522  chabs1  31548  chabs2  31549  spanun  31577  cmidi  31642  pjidmcoi  32209  csmdsymi  32366  sumdmdlem2  32451  dmdbr5ati  32454  mdcompli  32461  dmdcompli  32462  disjdifprg  32597  fcoinver  32626  f1rnen  32648  xppreima  32664  padct  32733  xrinfm  32761  clatp0cl  32949  clatp1cl  32950  xrsp0  32995  xrsp1  32996  cntrcrng  33046  gsumle  33074  cycpmconjslem1  33147  cycpmconjslem2  33148  gsumvsca1  33205  gsumvsca2  33206  qusxpid  33356  ellspds  33361  rspidlid  33368  rlmdim  33622  reff  33785  locfinreflem  33786  esumsnf  34028  esumcvg  34050  sigagenid  34115  iblidicc  34569  cxpcncf1  34572  fdvposlt  34576  fdvneggt  34577  fdvposle  34578  fdvnegge  34579  logdivsqrle  34627  bnj1253  34993  fineqvac  35073  cvmlift2lem6  35276  satfun  35379  mrsubrn  35481  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  imagesset  35917  ivthALT  36301  fness  36315  fneref  36316  refssfne  36324  fnemeet1  36332  fnejoin2  36335  filnetlem2  36345  filnetlem4  36347  ontgval  36397  knoppcnlem10  36468  knoppcnlem11  36469  bj-rabtr  36896  bj-rabtrAUTO  36898  bj-disj2r  36994  bj-restsnid  37053  bj-resta  37062  bj-imdirco  37156  elxp8  37337  finorwe  37348  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfposadd  37627  ftc1cnnclem  37651  ftc1cnnc  37652  ftc1anc  37661  ftc2nc  37662  areacirclem2  37669  areacirclem4  37671  areacirc  37673  caures  37720  constcncf  37722  brssrid  38458  brcnvssrid  38463  refrelid  38478  n0eldmqs  38604  atpsubN  39710  pol1N  39867  dia2dimlem13  41033  dibord  41116  dochvalr  41314  hdmapevec  41792  lcmineqlem10  41995  lcmineqlem12  41997  ismrcd1  42654  ismrc  42657  incssnn0  42667  mzpclall  42683  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  aomclem6  43016  kelac1  43020  gicabl  43056  arearect  43176  areaquad  43177  unielid  43180  oege2  43269  oacl2g  43292  ofoaf  43317  clcnvlem  43585  cnvtrcl0  43588  fvilbd  43651  relexp0a  43678  corcltrcl  43701  clsk1indlem2  44004  ntrclskb  44031  wnefimgd  44123  mnuprdlem4  44244  nzss  44286  lhe4.4ex1a  44298  dvsconst  44299  dvsid  44300  dvsef  44301  binomcxplemnn0  44318  onfrALTlem3  44515  onfrALTlem3VD  44858  unisn0  44956  founiiun0  45097  evthiccabs  45414  climconstmpt  45579  cncfshift  45795  addccncf2  45797  cncfcompt  45804  ioccncflimc  45806  icocncflimc  45810  cncfiooicclem1  45814  cncfiooicc  45815  cncfiooiccre  45816  cxpcncf2  45820  add1cncf  45822  add2cncf  45823  sub1cncfd  45824  sub2cncfd  45825  dvcosre  45833  dvmptfprod  45866  ibliooicc  45892  itgsincmulx  45895  itgsubsticclem  45896  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem16  46044  fourierdlem18  46046  fourierdlem21  46049  fourierdlem22  46050  fourierdlem23  46051  fourierdlem32  46060  fourierdlem33  46061  fourierdlem39  46067  fourierdlem40  46068  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem62  46089  fourierdlem68  46095  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem93  46120  fourierdlem94  46121  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  fouriercn  46153  etransclem18  46173  etransclem22  46177  etransclem34  46189  etransclem46  46201  etransclem47  46202  sge0fsum  46308  meaiininclem  46407  hoidmvlelem2  46517  hspdifhsp  46537  hspmbllem2  46548  hspmbl  46550  iinhoiicclem  46594  pimgtmnf2  46635  smflimsuplem1  46741  smflimsuplem6  46746  srhmsubcALTV  48048