MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssid Structured version   Visualization version   GIF version

Theorem ssid 3587
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.
StepHypRef Expression
1 id 22 . 2 (𝑥𝐴𝑥𝐴)
21ssriv 3572 1 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqimssi  3622  eqimss2i  3623  nsspssun  3819  difid  3902  inv1  3922  disjpss  3980  pwidg  4121  elssuni  4398  unimax  4404  intmin  4427  rintn0  4547  sseliALT  4714  xpss1  5140  xpss2  5141  residm  5337  resdm  5348  resmpt3  5357  ssrnres  5477  ordunidif  5676  dffn3  5953  fdmrn  5963  fvreseq1  6211  fimacnv  6240  iunpw  6848  onsucuni  6898  tfisi  6928  fparlem3  7144  fparlem4  7145  funsssuppss  7186  suppofss1d  7197  suppofss2d  7198  tfrlem1  7337  tz7.48-2  7402  oaordi  7491  omwordi  7516  omass  7525  nnaordi  7563  nnmwordi  7580  fpmg  7747  ralxpmap  7771  boxcutc  7815  domss2  7982  0fin  8051  en1eqsn  8053  findcard2d  8065  fimax2g  8069  domunfican  8096  pwfi  8122  fissuni  8132  fipreima  8133  fsuppmptif  8166  fsuppco2  8169  fsuppcor  8170  mapfienlem1  8171  mapfienlem2  8172  fimin2g  8264  wofib  8311  wemapso  8317  noinfep  8418  cantnfval2  8427  cantnfp1lem3  8438  cantnflem1  8447  tcidm  8483  tc0  8484  r1rankidb  8528  r1pw  8569  rankr1id  8586  scott0  8610  htalem  8620  xpomen  8699  infpwfien  8746  alephsmo  8786  dfac12lem3  8828  ackbij2lem4  8925  cflem  8929  cflecard  8936  cflim2  8946  cfslb  8949  fin4en1  8992  fin23lem13  9015  fin23lem15  9017  fin23lem36  9031  isf32lem1  9036  fin67  9078  dcomex  9130  zorn2lem4  9182  alephexp2  9260  fpwwe2lem13  9321  canthnumlem  9327  wunex2  9417  wuncidm  9425  eltsk2g  9430  axgroth6  9507  axgroth3  9510  xrsup  12487  expcl  12698  hashcard  12963  hashf1lem2  13052  xptrrel  13516  cotrtrclfv  13550  rtrclreclem1  13595  rtrclreclem2  13596  lo1eq  14096  rlimeq  14097  serclim0  14105  isercolllem2  14193  isercoll  14195  summolem3  14241  isum  14246  fsumser  14257  fsumcl  14260  fsum2d  14293  fsumabs  14323  fsumrlim  14333  fsumo1  14334  fsumiun  14343  flo1  14374  prodmolem3  14451  iprod  14456  iprodn0  14458  fprodss  14466  fprodcl  14470  fprod2d  14499  fprodclf  14511  risefaccl  14534  fallfaccl  14535  eflt  14635  rpnnen2lem3  14733  rpnnen2lem5  14735  rpnnen2lem11  14741  rpnnen2lem12  14742  rexpen  14745  eulerthlem2  15274  ressid  15711  ressinbas  15712  mremre  16036  catsubcat  16271  yon11  16676  yon12  16677  yon2  16678  yonpropd  16680  oppcyon  16681  yonffth  16696  oduclatb  16916  ipopos  16932  fpwipodrs  16936  submid  17123  mulgnncl  17328  mulgnnclOLD  17329  mulgnn0cl  17330  mulgcl  17331  subgid  17368  ghmghmrn  17451  cntrnsg  17546  symggen  17662  sylow3lem5  17818  lsmss1  17851  lsmss2  17853  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumadd  18095  gsumzmhm  18109  gsumzoppg  18116  gsum2dlem1  18141  gsum2dlem2  18142  gsum2d  18143  dprdfinv  18190  dprdf1  18204  dmdprdsplitlem  18208  dprd2db  18214  dpjidcl  18229  ablfac1eulem  18243  ablfac1eu  18244  ablfaclem2  18257  gsumdixp  18381  subrgid  18554  lcomfsupp  18675  lss1  18709  lbsextlem1  18928  rlmval2  18964  rlmbas  18965  rlmplusg  18966  rlm0  18967  rlmmulr  18969  rlmsca  18970  rlmsca2  18971  rlmvsca  18972  rlmtopn  18973  rlmds  18974  psrass1lem  19147  mplsubglem  19204  mpllsslem  19205  mplsubrglem  19209  mplcoe1  19235  mplcoe5  19238  mplbas2  19240  evlslem4  19278  psrbagev1  19280  evlslem2  19282  znf1o  19667  zntoslem  19672  regsumsupp  19735  css0  19800  uvcresum  19899  frlmsslsp  19902  frlmlbs  19903  frlmup1  19904  mamures  19963  mdetrsca2  20177  mdetrlin2  20180  mdetunilem5  20189  mdetunilem9  20193  smadiadetglem1  20244  smadiadetglem2  20245  pmatcollpw3  20356  cpmadumatpolylem2  20454  topopn  20484  fiinbas  20515  topbas  20535  topcld  20597  clstop  20631  ntrtop  20632  opnneissb  20676  opnssneib  20677  opnneiid  20688  neiptopuni  20692  neiptoptop  20693  maxlp  20709  isperf2  20714  restopn2  20739  restperf  20746  idcn  20819  cnconst2  20845  lmres  20862  rncmp  20957  fiuncmp  20965  cmpfi  20969  concn  20987  1stcelcls  21022  llyidm  21049  nllyidm  21050  toplly  21051  ssref  21073  refref  21074  kgentopon  21099  kgencn2  21118  ptpjpre1  21132  ptbasfi  21142  ptcld  21174  xkopt  21216  elqtop2  21262  qtopuni  21263  ptcmpfi  21374  fbssfi  21399  opnfbas  21404  filtop  21417  isfil2  21418  isfild  21420  fsubbas  21429  ssfg  21434  filssufilg  21473  ufileu  21481  imaelfm  21513  rnelfm  21515  fmfnfmlem4  21519  neiflim  21536  supnfcls  21582  fclscf  21587  flimfnfcls  21590  tsmsfbas  21689  utopbas  21797  xpsxmet  21943  xpsdsval  21944  xpsmet  21945  tmsxms  22049  tmsms  22050  imasf1oxms  22052  imasf1oms  22053  prdsxms  22093  prdsms  22094  tmsxpsval  22101  retopbas  22322  cnngp  22341  cnperf  22379  retopcon  22388  fsumcn  22429  abscncf  22460  recncf  22461  imcncf  22462  cjcncf  22463  mulc1cncf  22464  cncfcn1  22469  cncfmpt2f  22473  cncfmpt2ss  22474  addccncf  22475  cdivcncf  22476  negcncf  22477  negfcncf  22478  abscncfALT  22479  cnmpt2pc  22483  xrhmeo  22501  oprpiece1res1  22506  oprpiece1res2  22507  cnrehmeo  22508  iscau3  22829  caubl  22859  caublcls  22860  rrxcph  22933  rrxmval  22941  rrxdstprj1  22945  evthicc2  22981  ovolre  23045  volsuplem  23075  uniiccdif  23097  uniioovol  23098  uniiccvol  23099  uniioombllem3  23104  uniioombllem4  23105  uniioombllem5  23106  dyadmbllem  23118  volcn  23125  volivth  23126  itgfsum  23344  iblabslem  23345  iblabs  23346  bddmulibl  23356  cnlimc  23403  cnlimci  23404  dvres3  23428  dvres3a  23429  dvidlem  23430  dvcnp2  23434  dvcn  23435  dvnadd  23443  dvnres  23445  cpnord  23449  cpnres  23451  dvaddbr  23452  dvmulbr  23453  dvcmul  23458  dvcmulf  23459  dvcobr  23460  dvcjbr  23463  dvrec  23469  dvmptntr  23485  dvmptfsum  23487  dveflem  23491  dvef  23492  rolle  23502  dvlipcn  23506  c1liplem1  23508  dvgt0lem2  23515  dvivth  23522  lhop1lem  23525  dvfsumabs  23535  ftc1a  23549  ftc1cn  23555  ftc2  23556  deg1mul3le  23625  plyssc  23705  plyeq0  23716  coeeulem  23729  0dgr  23750  coemulc  23760  coe0  23761  coesub  23762  coe1termlem  23763  dgrmulc  23776  dgrsub  23777  dgrcolem1  23778  dgrcolem2  23779  dvnply2  23791  plycpn  23793  plyremlem  23808  fta1lem  23811  vieta1lem2  23815  aalioulem3  23838  dvntaylp  23874  taylthlem1  23876  taylthlem2  23877  ulmcn  23902  psercn  23929  pserdv  23932  abelth  23944  efcn  23946  efcvx  23952  pige3  24018  dvrelog  24128  logcn  24138  dvloglem  24139  dvlog  24142  dvlog2  24144  efopnlem2  24148  logccv  24154  cxpcn  24231  cxpcn2  24232  cxpcn3  24234  resqrtcn  24235  sqrtcn  24236  loglesqrt  24244  atancn  24408  rlimcnp3  24439  jensen  24460  lgamgulmlem2  24501  ftalem3  24546  basellem2  24553  dchrfi  24725  dchrisumlema  24922  pntrsumo1  24999  pntrsumbnd  25000  pntlem3  25043  cusgrasizeindslem1  25796  sspid  26758  ssps  26763  helch  27278  hhssnv  27299  hhsssh  27304  shintcl  27367  chintcl  27369  shlesb1i  27423  omlsi  27441  chlejb1i  27513  chm0i  27527  chabs1  27553  chabs2  27554  spanun  27582  cmidi  27647  pjidmcoi  28214  csmdsymi  28371  sumdmdlem2  28456  dmdbr5ati  28459  mdcompli  28466  dmdcompli  28467  disjdifprg  28564  fcoinver  28592  xppreima  28623  padct  28679  xrinfm  28703  clatp0cl  28796  clatp1cl  28797  xrsmulgzz  28803  xrsp0  28806  xrsp1  28807  gsumle  28904  gsummpt2co  28905  gsumvsca1  28907  gsumvsca2  28908  mdetpmtr1  29011  reff  29028  locfinreflem  29029  pnfneige0  29119  esumsnf  29247  esumcvg  29269  pwsiga  29314  sigagenid  29335  baselcarsg  29489  bnj1253  30133  cvmlift2lem6  30338  mrsubrn  30458  mrsubff1  30459  mrsub0  30461  mrsubccat  30463  mrsubcn  30464  elmrsubrn  30465  elmsubrn  30473  msubrn  30474  msubff1  30501  mthmpps  30527  trpredtr  30768  trpredpo  30773  wzel  30809  wzelOLD  30810  frrlem5c  30824  frrlem10  30829  imagesset  31024  ivthALT  31294  fness  31308  fneref  31309  refssfne  31317  fnemeet1  31325  fnejoin2  31328  filnetlem2  31338  filnetlem4  31340  ontgval  31394  knoppcnlem10  31456  knoppcnlem11  31457  knoppndvlem6  31472  knoppndv  31489  bj-rabtr  31912  bj-rabtrALTALT  31914  bj-rabtrAUTO  31915  bj-restsnid  32015  bj-restpw  32020  bj-restb  32022  bj-resta  32024  bj-restuni2  32026  elxp8  32189  mblfinlem3  32412  mblfinlem4  32413  ismblfin  32414  ovoliunnfl  32415  voliunnfl  32417  volsupnfl  32418  mbfposadd  32421  ftc1cnnclem  32447  ftc1cnnc  32448  ftc1anc  32457  ftc2nc  32458  areacirclem2  32465  areacirclem3  32466  areacirclem4  32467  areacirc  32469  welb  32495  caures  32520  constcncf  32522  idcncf  32523  sub1cncf  32524  sub2cncf  32525  cnresima  32527  rngoidl  32787  atpsubN  33851  pol1N  34008  1psubclN  34042  cdlemefrs32fva  34500  dia2dimlem13  35177  dibord  35260  dochvalr  35458  hdmapevec  35939  ismrcd1  36073  ismrc  36076  incssnn0  36086  mzpclall  36102  rmydioph  36393  rmxdioph  36395  expdiophlem2  36401  expdioph  36402  aomclem6  36441  kelac1  36445  gicabl  36481  rgspnid  36555  itgpowd  36613  arearect  36614  areaquad  36615  clcnvlem  36743  cnvtrucl0  36744  cnvtrcl0  36746  fvilbd  36794  relexp0a  36821  brfvrtrcld  36839  corcltrcl  36844  clsk3nimkb  37152  clsk1indlem2  37154  ntrclskb  37181  k0004ss2  37264  wnefimgd  37274  wfximgfd  37279  extoimad  37280  funfvima2d  37285  nzss  37332  lhe4.4ex1a  37344  dvsconst  37345  dvsid  37346  dvsef  37347  dvconstbi  37349  binomcxplemnn0  37364  onfrALTlem3  37574  onfrALTlem3VD  37939  cnopn  38027  unisn0  38041  ssinc  38086  ssdec  38087  founiiun  38149  founiiun0  38166  choicefi  38181  evthiccabs  38359  islptre  38480  climconstmpt  38519  fnlimfvre  38535  cncfshift  38553  addccncf2  38555  fsumcncf  38557  cncfperiod  38558  negcncfg  38560  cncfcompt  38562  ioccncflimc  38565  cncfuni  38566  icccncfext  38567  cncficcgt0  38568  icocncflimc  38569  cncfiooicclem1  38573  cncfiooicc  38574  cncfiooiccre  38575  cxpcncf2  38580  fprodcncf  38581  add1cncf  38582  add2cncf  38583  sub1cncfd  38584  sub2cncfd  38585  dvcosre  38593  dvcnre  38598  fperdvper  38602  dvmptresicc  38603  dvmptfprod  38629  itgsinexplem1  38639  itgcoscmulx  38655  ibliooicc  38657  itgsincmulx  38660  itgsubsticclem  38661  itgiccshift  38666  itgperiod  38667  itgsbtaddcnst  38668  dirkeritg  38789  dirkercncflem2  38791  dirkercncflem4  38793  fourierdlem16  38810  fourierdlem18  38812  fourierdlem21  38815  fourierdlem22  38816  fourierdlem23  38817  fourierdlem32  38826  fourierdlem33  38827  fourierdlem39  38833  fourierdlem40  38834  fourierdlem57  38850  fourierdlem58  38851  fourierdlem59  38852  fourierdlem62  38855  fourierdlem68  38861  fourierdlem72  38865  fourierdlem73  38866  fourierdlem74  38867  fourierdlem75  38868  fourierdlem76  38869  fourierdlem78  38871  fourierdlem83  38876  fourierdlem84  38877  fourierdlem85  38878  fourierdlem88  38881  fourierdlem93  38886  fourierdlem94  38887  fourierdlem95  38888  fourierdlem97  38890  fourierdlem101  38894  fourierdlem103  38896  fourierdlem104  38897  fourierdlem111  38904  fourierdlem112  38905  fourierdlem113  38906  sqwvfoura  38915  sqwvfourb  38916  fouriersw  38918  fouriercn  38919  etransclem18  38939  etransclem22  38943  etransclem34  38955  etransclem46  38967  etransclem47  38968  sge0fsum  39074  meaiininclem  39170  hoidmvlelem2  39280  hspdifhsp  39300  hspmbllem2  39311  hspmbl  39313  iinhoiicclem  39358  pimgtmnf2  39395  funresfunco  39648  uhgrsubgrself  40496  uhgrspansubgr  40507  nbupgr  40558  nbumgrvtx  40560  nbgr2vtx1edg  40564  cusgrexi  40654  1wlkvtxeledglem  40819  umgr2adedgwlk  41144  umgr2adedgwlkon  41145  umgr2adedgspth  41147  upgr11wlkdlem2  41305  1pthon2ve  41313  submgmid  41575  rnghmsscmap2  41757  rhmsscmap2  41803  srhmsubc  41860  fldhmsubc  41868  srhmsubcALTV  41879  fldhmsubcALTV  41887  elbigolo1  42141
  Copyright terms: Public domain W3C validator