Theorem ssid 3930

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

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895

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

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

This theorem is used by:  ssidd  3931  eqimssd  3964  eqimsscd  3965  eqimssi  3968  eqimss2i  3969  nsspssun  4213  difidALT  4325  inv1  4347  disjpss  4413  disjdif  4425  pwidgOLD  4578  elssuni  4898  unimax  4904  intmin  4927  rintn0  5068  sseliALT  5262  inxpssres  5667  xpss1  5669  xpss2  5670  residm  6000  resdm  6014  resmpt3  6029  imadmrn  6066  cnvimarndm  6079  cnvrescnv  6187  imadifssrn  6201  onelssex  6412  ordunidif  6413  funresfunco  6582  dffn3  6723  fdmrn  6742  fvreseq1  7039  iunpw  7786  onsucuni  7840  tfisi  7871  fparlem3  8128  fparlem4  8129  funsssuppss  8211  tfrlem1  8387  tz7.48-2  8456  oaordi  8558  omwordi  8583  omass  8592  nnaordi  8631  nnmwordi  8648  naddunif  8707  fpmg  8900  boxcutc  8973  domss2  9159  findcard2d  9186  fimax2g  9281  domunfican  9317  fipreima  9351  fimin2g  9495  wofib  9543  wemapso  9549  noinfep  9665  cantnfval2  9674  tcidm  9749  tc0  9750  r1rankidb  9816  r1pw  9863  rankr1id  9882  scott0b  9941  scott0OLD  9942  xpomen  10098  infpwfien  10145  alephsmo  10185  dfac12lem3  10228  cflem  10327  cflecard  10334  cfslb  10348  fin4en1  10391  fin23lem13  10414  fin23lem36  10430  isf32lem1  10435  fin67  10477  dcomex  10529  zorn2lem4  10581  alephexp2  10670  fpwwe2lem12  10731  canthnumlem  10737  wuncidm  10835  eltsk2g  10840  axgroth6  10917  axgroth3  10920  indconst1  12337  xrsup  14012  expcl  14226  hashcard  14503  hashf1lem2  14605  xptrrel  15139  cotrtrclfv  15171  rtrclreclem2  15218  lo1eq  15741  rlimeq  15742  serclim0  15750  isercolllem2  15839  isercoll  15841  fsum2d  15943  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  fprod2d  16154  risefaccl  16188  fallfaccl  16189  eflt  16291  rpnnen2lem3  16390  rpnnen2lem5  16392  rpnnen2lem12  16399  rexpen  16402  ressbasssg  17421  ressid  17428  ressinbas  17429  oduclatb  18687  ipopos  18716  fpwipodrs  18720  qusxpid  19401  ghmghmrn  19455  elcntr  19550  cntrnsg  19564  0symgefmndeq  19614  sylow3lem5  19851  lsmss1  19885  lsmss2  19887  cmnbascntr  20025  cntrcmnd  20062  cntrabl  20063  gsumzres  20129  gsumzcl2  20130  gsumzf1o  20132  gsumadd  20143  gsumzmhm  20157  gsumzoppg  20164  dprdf1  20255  ablfac1eulem  20294  gsumle  20365  subrgid  20831  srhmsubc  20938  lbsextlem1  21442  rlmval2  21473  znf1o  21863  zntoslem  21868  css0  22001  uvcresum  22105  frlmlbs  22109  psrass1lem  22247  mdetrsca2  22925  mdetrlin2  22928  mdetunilem5  22937  mdetunilem9  22941  smadiadetglem1  22992  smadiadetglem2  22993  pmatcollpw3  23108  topopn  23230  fiinbas  23276  topbas  23296  topcld  23359  ntrtop  23394  opnneissb  23438  opnssneib  23439  opnneiid  23450  maxlp  23471  isperf2  23476  restperf  23508  idcn  23581  cnconst2  23607  lmres  23624  fiuncmp  23728  1stcelcls  23786  ssref  23837  refref  23838  kgencn2  23882  ptpjpre1  23896  ptbasfi  23906  xkopt  23980  elqtop2  24026  ptcmpfi  24138  fbssfi  24162  opnfbas  24167  filtop  24180  isfil2  24181  isfild  24183  fsubbas  24192  ssfg  24197  filssufilg  24236  ufileu  24244  imaelfm  24276  rnelfm  24278  fmfnfmlem4  24282  neiflim  24299  fclscf  24350  flimfnfcls  24353  tsmsfbas  24453  xpsxmet  24705  xpsdsval  24706  xpsmet  24707  tmsxms  24811  tmsms  24812  imasf1oxms  24814  imasf1oms  24815  prdsxms  24855  prdsms  24856  tmsxpsval  24863  retopbas  25085  cnngp  25104  cnopn  25111  cnperf  25146  retopconn  25155  fsumcn  25197  abscncf  25228  recncf  25229  imcncf  25230  cjcncf  25231  mulc1cncf  25232  cncfcn1  25238  cncfmpt2f  25242  cncfmpt2ss  25243  addccncf  25244  idcncf  25245  sub1cncf  25246  sub2cncf  25247  cdivcncf  25248  negcncf  25249  negfcncf  25250  abscncfALT  25251  cnmpopc  25255  xrhmeo  25273  oprpiece1res1  25278  oprpiece1res2  25279  cnrehmeo  25280  iscau3  25605  caubl  25635  caublcls  25636  mulcncf  25773  evthicc2  25787  ovolre  25852  volsuplem  25882  uniiccdif  25905  uniioovol  25906  uniiccvol  25907  uniioombllem3  25912  uniioombllem4  25913  uniioombllem5  25914  dyadmbllem  25926  volivth  25934  itgfsum  26153  iblabslem  26154  iblabs  26155  bddmulibl  26165  cnlimc  26214  cnlimci  26215  dvcnp2  26246  dvcn  26247  cpnord  26261  cpnres  26263  dvmptntr  26297  dvmptfsum  26301  rolle  26316  dvlipcn  26320  c1liplem1  26322  dvivth  26336  dvfsumabs  26349  ftc1a  26363  ftc1cn  26369  plyssc  26524  plyeq0  26536  0dgr  26570  coemulc  26580  coe0  26581  coesub  26582  coe1termlem  26583  dgrmulc  26596  dgrsub  26597  dvnply2  26614  plycpn  26616  plyremlem  26631  fta1lem  26634  vieta1lem2  26640  aalioulem3  26667  taylthlem1  26706  taylthlem2  26707  ulmcn  26732  psercn  26759  abelth  26774  efcn  26776  efcvx  26782  dvrelog  26971  logcn  26981  dvloglem  26982  dvlog  26985  dvlog2  26987  efopnlem2  26991  logccv  26997  cxpcn  27079  cxpcn3  27082  resqrtcn  27083  sqrtcn  27084  loglesqrt  27095  atancn  27270  jensen  27322  ftalem3  27408  dchrfi  27588  dchrisumlema  27821  pntlem3  27942  madebday  28292  expscl  28823  bdaypw2n0bndlem  28855  uhgrsubgrself  29867  uhgrspansubgr  29878  umgr2adedgwlk  30540  umgr2adedgwlkon  30541  umgr2adedgspth  30543  upgr1wlkdlem2  30743  sspid  31333  ssps  31338  helch  31851  hhssnv  31872  hhsssh  31877  shintcl  31938  chintcl  31940  shlesb1i  31994  omlsi  32012  chlejb1i  32084  chm0i  32098  chabs1  32124  chabs2  32125  spanun  32153  cmidi  32218  pjidmcoi  32785  csmdsymi  32942  sumdmdlem2  33027  dmdbr5ati  33030  mdcompli  33037  dmdcompli  33038  disjdifprg  33217  fcoinver  33246  f1rnen  33270  xppreima  33287  padct  33358  xrinfm  33394  clatp0cl  33584  clatp1cl  33585  xrsp0  33620  xrsp1  33621  cntrcrng  33689  cycpmconjslem1  33762  cycpmconjslem2  33763  gsumvsca1  33834  gsumvsca2  33835  ellspds  33971  rspidlid  33977  rlmdim  34289  locfinreflem  34519  esumsnf  34743  esumcvg  34765  sigagenid  34831  iblidicc  35268  cxpcncf1  35271  fdvposlt  35275  fdvneggt  35276  fdvposle  35277  fdvnegge  35278  logdivsqrle  35326  bnj1253  35694  fineqvac  35841  fineqvnttrclse  35849  noinfepfnregs  35857  prconf1acwevd  35968  cvmlift2lem6  36160  satfun  36263  mrsubrn  36365  elmrsubrn  36372  elmsubrn  36380  msubrn  36381  imagesset  36810  nmuladdss  37055  ivthALT  37216  fness  37230  fneref  37231  refssfne  37239  fnemeet1  37247  fnejoin2  37250  filnetlem2  37260  filnetlem4  37262  ontgval  37312  ttctrid  37383  knoppcnlem10  37461  knoppcnlem11  37462  bj-rabtr  37936  bj-rabtrAUTO  37938  bj-disj2r  38034  bj-restsnid  38101  bj-resta  38110  bj-imdirco  38205  elxp8  38388  finorwe  38399  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  mbfposadd  38679  ftc1cnnclem  38703  ftc1cnnc  38704  ftc1anc  38713  ftc2nc  38714  areacirclem2  38721  areacirclem4  38723  areacirc  38725  caures  38788  constcncf  38790  brssrid  39608  brcnvssrid  39613  refrelid  39628  n0eldmqs  39758  atpsubN  40904  pol1N  41061  dia2dimlem13  42227  dibord  42310  dochvalr  42508  hdmapevec  42986  lcmineqlem10  43182  lcmineqlem12  43184  ismrcd1  43803  ismrc  43806  incssnn0  43816  mzpclall  43832  rmydioph  44115  rmxdioph  44117  expdiophlem2  44123  expdioph  44124  aomclem6  44155  kelac1  44159  gicabl  44195  arearect  44311  areaquad  44312  unielid  44315  oege2  44403  oacl2g  44426  ofoaf  44451  clcnvlem  44717  cnvtrcl0  44720  fvilbd  44783  relexp0a  44810  corcltrcl  44833  clsk1indlem2  45136  ntrclskb  45163  wnefimgd  45255  mnuprdlem4  45353  nzss  45395  lhe4.4ex1a  45407  dvsconst  45408  dvsid  45409  dvsef  45410  binomcxplemnn0  45427  onfrALTlem3  45621  onfrALTlem3VD  45963  unisn0  46165  founiiun0  46299  evthiccabs  46602  climconstmpt  46762  cncfshift  46978  addccncf2  46980  cncfcompt  46987  ioccncflimc  46989  icocncflimc  46993  cncfiooicclem1  46997  cncfiooicc  46998  cncfiooiccre  46999  cxpcncf2  47003  add1cncf  47005  add2cncf  47006  sub1cncfd  47007  sub2cncfd  47008  dvcosre  47016  dvmptfprod  47049  ibliooicc  47075  itgsincmulx  47078  itgsubsticclem  47079  itgiccshift  47084  itgperiod  47085  itgsbtaddcnst  47086  dirkeritg  47206  dirkercncflem2  47208  dirkercncflem4  47210  fourierdlem16  47227  fourierdlem18  47229  fourierdlem21  47232  fourierdlem22  47233  fourierdlem23  47234  fourierdlem32  47243  fourierdlem33  47244  fourierdlem39  47250  fourierdlem40  47251  fourierdlem57  47267  fourierdlem58  47268  fourierdlem59  47269  fourierdlem62  47272  fourierdlem68  47278  fourierdlem72  47282  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem78  47288  fourierdlem83  47293  fourierdlem84  47294  fourierdlem85  47295  fourierdlem88  47298  fourierdlem93  47303  fourierdlem94  47304  fourierdlem95  47305  fourierdlem97  47307  fourierdlem101  47311  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fourierdlem112  47322  sqwvfoura  47332  sqwvfourb  47333  fouriersw  47335  fouriercn  47336  etransclem18  47356  etransclem22  47360  etransclem34  47372  etransclem46  47384  etransclem47  47385  sge0fsum  47491  meaiininclem  47590  hoidmvlelem2  47700  hspdifhsp  47720  hspmbllem2  47731  hspmbl  47733  iinhoiicclem  47777  pimgtmnf2  47818  smflimsuplem1  47924  smflimsuplem6  47929  cjnpoly  48033  sqrtnpoly  48037  srhmsubcALTV  49516  imaidfu2lem  50319  imaidfu  50320  imaidfu2  50321  setc1onsubc  50834  dvsec  51025  dvcsc  51026  dvcot  51027