Theorem ssid 3935

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 23	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
2	1	ssriv 3917	1 ⊢ 𝐴 ⊆ 𝐴

This proof depends on syntax axioms:   ∈ wcel 2147   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ss 3901

This theorem is used by:  ssidd  3936  eqimssd  3969  eqimsscd  3970  eqimssi  3973  eqimss2i  3974  nsspssun  4216  difidALT  4329  inv1  4351  disjpss  4417  disjdif  4429  pwidgOLD  4582  elssuni  4902  unimax  4908  intmin  4931  rintn0  5072  sseliALT  5267  inxpssres  5673  xpss1  5675  xpss2  5676  residm  6014  resdm  6028  resmpt3  6043  imadmrn  6080  cnvimarndm  6093  cnvrescnv  6201  imadifssrn  6215  onelssex  6433  ordunidif  6434  funresfunco  6604  dffn3  6747  fdmrn  6766  fvreseq1  7064  iunpw  7812  onsucuni  7866  tfisi  7897  fparlem3  8155  fparlem4  8156  funsssuppss  8238  tfrlem1  8414  tz7.48-2  8483  oaordi  8585  omwordi  8610  omass  8619  nnaordi  8658  nnmwordi  8675  naddunif  8734  fpmg  8927  boxcutc  9000  domss2  9186  findcard2d  9213  fimax2g  9308  domunfican  9344  fipreima  9378  fimin2g  9521  wofib  9569  wemapso  9575  noinfep  9691  cantnfval2  9700  tcidm  9775  tc0  9776  r1rankidb  9842  r1pw  9889  rankr1id  9908  scott0b  9967  scott0OLD  9968  xpomen  10124  infpwfien  10171  alephsmo  10211  dfac12lem3  10254  cflem  10353  cflecard  10360  cfslb  10374  fin4en1  10417  fin23lem13  10440  fin23lem36  10456  isf32lem1  10461  fin67  10503  dcomex  10555  zorn2lem4  10607  alephexp2  10696  fpwwe2lem12  10757  canthnumlem  10763  wuncidm  10861  eltsk2g  10866  axgroth6  10943  axgroth3  10946  indconst1  12363  xrsup  14038  expcl  14252  hashcard  14529  hashf1lem2  14631  xptrrel  15165  cotrtrclfv  15197  rtrclreclem2  15244  lo1eq  15767  rlimeq  15768  serclim0  15776  isercolllem2  15865  isercoll  15867  fsum2d  15969  fsumabs  16000  fsumrlim  16010  fsumo1  16011  fsumiun  16020  fprod2d  16180  risefaccl  16214  fallfaccl  16215  eflt  16317  rpnnen2lem3  16416  rpnnen2lem5  16418  rpnnen2lem12  16425  rexpen  16428  ressbasssg  17447  ressid  17454  ressinbas  17455  oduclatb  18713  ipopos  18742  fpwipodrs  18746  qusxpid  19427  ghmghmrn  19481  elcntr  19577  cntrnsg  19591  0symgefmndeq  19641  sylow3lem5  19878  lsmss1  19912  lsmss2  19914  cmnbascntr  20052  cntrcmnd  20089  cntrabl  20090  gsumzres  20156  gsumzcl2  20157  gsumzf1o  20159  gsumadd  20170  gsumzmhm  20184  gsumzoppg  20191  dprdf1  20282  ablfac1eulem  20321  gsumle  20392  subrgid  20858  srhmsubc  20965  lbsextlem1  21469  rlmval2  21500  znf1o  21890  zntoslem  21895  css0  22028  uvcresum  22132  frlmlbs  22136  psrass1lem  22274  mdetrsca2  22952  mdetrlin2  22955  mdetunilem5  22964  mdetunilem9  22968  smadiadetglem1  23019  smadiadetglem2  23020  pmatcollpw3  23135  topopn  23257  fiinbas  23303  topbas  23323  topcld  23386  ntrtop  23421  opnneissb  23465  opnssneib  23466  opnneiid  23477  maxlp  23498  isperf2  23503  restperf  23535  idcn  23608  cnconst2  23634  lmres  23651  fiuncmp  23755  1stcelcls  23813  ssref  23864  refref  23865  kgencn2  23909  ptpjpre1  23923  ptbasfi  23933  xkopt  24007  elqtop2  24053  ptcmpfi  24165  fbssfi  24189  opnfbas  24194  filtop  24207  isfil2  24208  isfild  24210  fsubbas  24219  ssfg  24224  filssufilg  24263  ufileu  24271  imaelfm  24303  rnelfm  24305  fmfnfmlem4  24309  neiflim  24326  fclscf  24377  flimfnfcls  24380  tsmsfbas  24480  xpsxmet  24732  xpsdsval  24733  xpsmet  24734  tmsxms  24838  tmsms  24839  imasf1oxms  24841  imasf1oms  24842  prdsxms  24882  prdsms  24883  tmsxpsval  24890  retopbas  25112  cnngp  25131  cnopn  25138  cnperf  25173  retopconn  25182  fsumcn  25224  abscncf  25255  recncf  25256  imcncf  25257  cjcncf  25258  mulc1cncf  25259  cncfcn1  25265  cncfmpt2f  25269  cncfmpt2ss  25270  addccncf  25271  idcncf  25272  sub1cncf  25273  sub2cncf  25274  cdivcncf  25275  negcncf  25276  negfcncf  25277  abscncfALT  25278  cnmpopc  25282  xrhmeo  25300  oprpiece1res1  25305  oprpiece1res2  25306  cnrehmeo  25307  iscau3  25632  caubl  25662  caublcls  25663  mulcncf  25800  evthicc2  25814  ovolre  25879  volsuplem  25909  uniiccdif  25932  uniioovol  25933  uniiccvol  25934  uniioombllem3  25939  uniioombllem4  25940  uniioombllem5  25941  dyadmbllem  25953  volivth  25961  itgfsum  26180  iblabslem  26181  iblabs  26182  bddmulibl  26192  cnlimc  26241  cnlimci  26242  dvcnp2  26273  dvcn  26274  cpnord  26288  cpnres  26290  dvmptntr  26324  dvmptfsum  26328  rolle  26343  dvlipcn  26347  c1liplem1  26349  dvivth  26363  dvfsumabs  26376  ftc1a  26390  ftc1cn  26396  plyssc  26551  plyeq0  26563  0dgr  26597  coemulc  26607  coe0  26608  coesub  26609  coe1termlem  26610  dgrmulc  26623  dgrsub  26624  dvnply2  26641  plycpn  26643  plyremlem  26658  fta1lem  26661  vieta1lem2  26667  aalioulem3  26694  taylthlem1  26733  taylthlem2  26734  ulmcn  26759  psercn  26786  abelth  26801  efcn  26803  efcvx  26809  dvrelog  26998  logcn  27008  dvloglem  27009  dvlog  27012  dvlog2  27014  efopnlem2  27018  logccv  27024  cxpcn  27106  cxpcn3  27109  resqrtcn  27110  sqrtcn  27111  loglesqrt  27122  atancn  27297  jensen  27349  ftalem3  27435  dchrfi  27615  dchrisumlema  27848  pntlem3  27969  madebday  28319  expscl  28850  bdaypw2n0bndlem  28882  uhgrsubgrself  29894  uhgrspansubgr  29905  umgr2adedgwlk  30567  umgr2adedgwlkon  30568  umgr2adedgspth  30570  upgr1wlkdlem2  30770  sspid  31360  ssps  31365  helch  31878  hhssnv  31899  hhsssh  31904  shintcl  31965  chintcl  31967  shlesb1i  32021  omlsi  32039  chlejb1i  32111  chm0i  32125  chabs1  32151  chabs2  32152  spanun  32180  cmidi  32245  pjidmcoi  32812  csmdsymi  32969  sumdmdlem2  33054  dmdbr5ati  33057  mdcompli  33064  dmdcompli  33065  disjdifprg  33244  fcoinver  33273  f1rnen  33297  xppreima  33314  padct  33384  xrinfm  33420  clatp0cl  33610  clatp1cl  33611  xrsp0  33649  xrsp1  33650  cntrcrng  33718  cycpmconjslem1  33791  cycpmconjslem2  33792  gsumvsca1  33863  gsumvsca2  33864  ellspds  34008  rspidlid  34014  rlmdim  34325  locfinreflem  34555  esumsnf  34779  esumcvg  34801  sigagenid  34867  iblidicc  35304  cxpcncf1  35307  fdvposlt  35311  fdvneggt  35312  fdvposle  35313  fdvnegge  35314  logdivsqrle  35362  bnj1253  35730  fineqvac  35897  fineqvnttrclse  35905  noinfepfnregs  35913  prconf1acwevd  36061  cvmlift2lem6  36253  satfun  36356  mrsubrn  36458  elmrsubrn  36465  elmsubrn  36473  msubrn  36474  imagesset  36908  nmuladdss  37153  ivthALT  37314  fness  37328  fneref  37329  refssfne  37337  fnemeet1  37345  fnejoin2  37348  filnetlem2  37358  filnetlem4  37360  ontgval  37410  ttctrid  37481  knoppcnlem10  37559  knoppcnlem11  37560  bj-rabtr  38034  bj-rabtrAUTO  38036  bj-disj2r  38132  bj-restsnid  38212  bj-resta  38221  bj-imdirco  38316  elxp8  38499  finorwe  38510  mblfinlem3  38782  mblfinlem4  38783  ismblfin  38784  ovoliunnfl  38785  voliunnfl  38787  volsupnfl  38788  mbfposadd  38790  ftc1cnnclem  38814  ftc1cnnc  38815  ftc1anc  38824  ftc2nc  38825  areacirclem2  38832  areacirclem4  38834  areacirc  38836  caures  38897  constcncf  38899  brssrid  39717  brcnvssrid  39722  refrelid  39737  n0eldmqs  39867  atpsubN  41013  pol1N  41170  dia2dimlem13  42336  dibord  42419  dochvalr  42617  hdmapevec  43095  lcmineqlem10  43291  lcmineqlem12  43293  ismrcd1  43913  ismrc  43916  incssnn0  43926  mzpclall  43942  rmydioph  44225  rmxdioph  44227  expdiophlem2  44233  expdioph  44234  aomclem6  44265  kelac1  44269  gicabl  44305  arearect  44420  areaquad  44421  unielid  44424  oege2  44512  oacl2g  44535  ofoaf  44560  clcnvlem  44826  cnvtrcl0  44829  fvilbd  44892  relexp0a  44919  corcltrcl  44942  clsk1indlem2  45245  ntrclskb  45272  wnefimgd  45364  mnuprdlem4  45462  nzss  45504  lhe4.4ex1a  45516  dvsconst  45517  dvsid  45518  dvsef  45519  binomcxplemnn0  45536  onfrALTlem3  45729  onfrALTlem3VD  46071  unisn0  46287  founiiun0  46420  evthiccabs  46723  climconstmpt  46883  cncfshift  47099  addccncf2  47101  cncfcompt  47108  ioccncflimc  47110  icocncflimc  47114  cncfiooicclem1  47118  cncfiooicc  47119  cncfiooiccre  47120  cxpcncf2  47124  add1cncf  47126  add2cncf  47127  sub1cncfd  47128  sub2cncfd  47129  dvcosre  47137  dvmptfprod  47170  ibliooicc  47196  itgsincmulx  47199  itgsubsticclem  47200  itgiccshift  47205  itgperiod  47206  itgsbtaddcnst  47207  dirkeritg  47327  dirkercncflem2  47329  dirkercncflem4  47331  fourierdlem16  47348  fourierdlem18  47350  fourierdlem21  47353  fourierdlem22  47354  fourierdlem23  47355  fourierdlem32  47364  fourierdlem33  47365  fourierdlem39  47371  fourierdlem40  47372  fourierdlem57  47388  fourierdlem58  47389  fourierdlem59  47390  fourierdlem62  47393  fourierdlem68  47399  fourierdlem72  47403  fourierdlem73  47404  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem78  47409  fourierdlem83  47414  fourierdlem84  47415  fourierdlem85  47416  fourierdlem88  47419  fourierdlem93  47424  fourierdlem94  47425  fourierdlem95  47426  fourierdlem97  47428  fourierdlem101  47432  fourierdlem103  47434  fourierdlem104  47435  fourierdlem111  47442  fourierdlem112  47443  sqwvfoura  47453  sqwvfourb  47454  fouriersw  47456  fouriercn  47457  etransclem18  47477  etransclem22  47481  etransclem34  47493  etransclem46  47505  etransclem47  47506  sge0fsum  47612  meaiininclem  47711  hoidmvlelem2  47821  hspdifhsp  47841  hspmbllem2  47852  hspmbl  47854  iinhoiicclem  47898  pimgtmnf2  47939  smflimsuplem1  48045  smflimsuplem6  48050  cjnpoly  48154  sqrtnpoly  48158  srhmsubcALTV  49637  imaidfu2lem  50440  imaidfu  50441  imaidfu2  50442  setc1onsubc  50955  dvsec  51168  dvcsc  51169  dvcot  51170