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  4403  unimax  4409  intmin  4432  rintn0  4552  sseliALT  4719  xpss1  5151  xpss2  5152  residm  5350  resdm  5361  resmpt3  5370  ssrnres  5491  ordunidif  5690  dffn3  5967  fdmrn  5977  fvreseq1  6226  fimacnv  6255  iunpw  6870  onsucuni  6920  tfisi  6950  fparlem3  7166  fparlem4  7167  funsssuppss  7208  suppofss1d  7219  suppofss2d  7220  tfrlem1  7359  tz7.48-2  7424  oaordi  7513  omwordi  7538  omass  7547  nnaordi  7585  nnmwordi  7602  fpmg  7769  ralxpmap  7793  boxcutc  7837  domss2  8004  0fin  8073  en1eqsn  8075  findcard2d  8087  fimax2g  8091  domunfican  8118  pwfi  8144  fissuni  8154  fipreima  8155  fsuppmptif  8188  fsuppco2  8191  fsuppcor  8192  mapfienlem1  8193  mapfienlem2  8194  fimin2g  8286  wofib  8333  wemapso  8339  noinfep  8440  cantnfval2  8449  cantnfp1lem3  8460  cantnflem1  8469  tcidm  8505  tc0  8506  r1rankidb  8550  r1pw  8591  rankr1id  8608  scott0  8632  htalem  8642  xpomen  8721  infpwfien  8768  alephsmo  8808  dfac12lem3  8850  ackbij2lem4  8947  cflem  8951  cflecard  8958  cflim2  8968  cfslb  8971  fin4en1  9014  fin23lem13  9037  fin23lem15  9039  fin23lem36  9053  isf32lem1  9058  fin67  9100  dcomex  9152  zorn2lem4  9204  alephexp2  9282  fpwwe2lem13  9343  canthnumlem  9349  wunex2  9439  wuncidm  9447  eltsk2g  9452  axgroth6  9529  axgroth3  9532  xrsup  12529  expcl  12740  hashcard  13008  hashf1lem2  13097  xptrrel  13567  cotrtrclfv  13601  rtrclreclem1  13646  rtrclreclem2  13647  lo1eq  14147  rlimeq  14148  serclim0  14156  isercolllem2  14244  isercoll  14246  summolem3  14292  isum  14297  fsumser  14308  fsumcl  14311  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  flo1  14425  prodmolem3  14502  iprod  14507  iprodn0  14509  fprodss  14517  fprodcl  14521  fprod2d  14550  fprodclf  14562  risefaccl  14585  fallfaccl  14586  eflt  14686  rpnnen2lem3  14784  rpnnen2lem5  14786  rpnnen2lem11  14792  rpnnen2lem12  14793  rexpen  14796  eulerthlem2  15325  ressid  15762  ressinbas  15763  mremre  16087  catsubcat  16322  yon11  16727  yon12  16728  yon2  16729  yonpropd  16731  oppcyon  16732  yonffth  16747  oduclatb  16967  ipopos  16983  fpwipodrs  16987  submid  17174  mulgnncl  17379  mulgnnclOLD  17380  mulgnn0cl  17381  mulgcl  17382  subgid  17419  ghmghmrn  17502  cntrnsg  17597  symggen  17713  sylow3lem5  17869  lsmss1  17902  lsmss2  17904  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumadd  18146  gsumzmhm  18160  gsumzoppg  18167  gsum2dlem1  18192  gsum2dlem2  18193  gsum2d  18194  dprdfinv  18241  dprdf1  18255  dmdprdsplitlem  18259  dprd2db  18265  dpjidcl  18280  ablfac1eulem  18294  ablfac1eu  18295  ablfaclem2  18308  gsumdixp  18432  subrgid  18605  lcomfsupp  18726  lss1  18760  lbsextlem1  18979  rlmval2  19015  rlmbas  19016  rlmplusg  19017  rlm0  19018  rlmmulr  19020  rlmsca  19021  rlmsca2  19022  rlmvsca  19023  rlmtopn  19024  rlmds  19025  psrass1lem  19198  mplsubglem  19255  mpllsslem  19256  mplsubrglem  19260  mplcoe1  19286  mplcoe5  19289  mplbas2  19291  evlslem4  19329  psrbagev1  19331  evlslem2  19333  znf1o  19719  zntoslem  19724  regsumsupp  19787  css0  19852  uvcresum  19951  frlmsslsp  19954  frlmlbs  19955  frlmup1  19956  mamures  20015  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  mdetunilem9  20245  smadiadetglem1  20296  smadiadetglem2  20297  pmatcollpw3  20408  cpmadumatpolylem2  20506  topopn  20536  fiinbas  20567  topbas  20587  topcld  20649  clstop  20683  ntrtop  20684  opnneissb  20728  opnssneib  20729  opnneiid  20740  neiptopuni  20744  neiptoptop  20745  maxlp  20761  isperf2  20766  restopn2  20791  restperf  20798  idcn  20871  cnconst2  20897  lmres  20914  rncmp  21009  fiuncmp  21017  cmpfi  21021  concn  21039  1stcelcls  21074  llyidm  21101  nllyidm  21102  toplly  21103  ssref  21125  refref  21126  kgentopon  21151  kgencn2  21170  ptpjpre1  21184  ptbasfi  21194  ptcld  21226  xkopt  21268  elqtop2  21314  qtopuni  21315  ptcmpfi  21426  fbssfi  21451  opnfbas  21456  filtop  21469  isfil2  21470  isfild  21472  fsubbas  21481  ssfg  21486  filssufilg  21525  ufileu  21533  imaelfm  21565  rnelfm  21567  fmfnfmlem4  21571  neiflim  21588  supnfcls  21634  fclscf  21639  flimfnfcls  21642  tsmsfbas  21741  utopbas  21849  xpsxmet  21995  xpsdsval  21996  xpsmet  21997  tmsxms  22101  tmsms  22102  imasf1oxms  22104  imasf1oms  22105  prdsxms  22145  prdsms  22146  tmsxpsval  22153  retopbas  22374  cnngp  22393  cnperf  22431  retopcon  22440  fsumcn  22481  abscncf  22512  recncf  22513  imcncf  22514  cjcncf  22515  mulc1cncf  22516  cncfcn1  22521  cncfmpt2f  22525  cncfmpt2ss  22526  addccncf  22527  cdivcncf  22528  negcncf  22529  negfcncf  22530  abscncfALT  22531  cnmpt2pc  22535  xrhmeo  22553  oprpiece1res1  22558  oprpiece1res2  22559  cnrehmeo  22560  iscau3  22884  caubl  22914  caublcls  22915  rrxcph  22988  rrxmval  22996  rrxdstprj1  23000  evthicc2  23036  ovolre  23100  volsuplem  23130  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  dyadmbllem  23173  volcn  23180  volivth  23181  itgfsum  23399  iblabslem  23400  iblabs  23401  bddmulibl  23411  cnlimc  23458  cnlimci  23459  dvres3  23483  dvres3a  23484  dvidlem  23485  dvcnp2  23489  dvcn  23490  dvnadd  23498  dvnres  23500  cpnord  23504  cpnres  23506  dvaddbr  23507  dvmulbr  23508  dvcmul  23513  dvcmulf  23514  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvmptntr  23540  dvmptfsum  23542  dveflem  23546  dvef  23547  rolle  23557  dvlipcn  23561  c1liplem1  23563  dvgt0lem2  23570  dvivth  23577  lhop1lem  23580  dvfsumabs  23590  ftc1a  23604  ftc1cn  23610  ftc2  23611  deg1mul3le  23680  plyssc  23760  plyeq0  23771  coeeulem  23784  0dgr  23805  coemulc  23815  coe0  23816  coesub  23817  coe1termlem  23818  dgrmulc  23831  dgrsub  23832  dgrcolem1  23833  dgrcolem2  23834  dvnply2  23846  plycpn  23848  plyremlem  23863  fta1lem  23866  vieta1lem2  23870  aalioulem3  23893  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  ulmcn  23957  psercn  23984  pserdv  23987  abelth  23999  efcn  24001  efcvx  24007  pige3  24073  dvrelog  24183  logcn  24193  dvloglem  24194  dvlog  24197  dvlog2  24199  efopnlem2  24203  logccv  24209  cxpcn  24286  cxpcn2  24287  cxpcn3  24289  resqrtcn  24290  sqrtcn  24291  loglesqrt  24299  atancn  24463  rlimcnp3  24494  jensen  24515  lgamgulmlem2  24556  ftalem3  24601  basellem2  24608  dchrfi  24780  dchrisumlema  24977  pntrsumo1  25054  pntrsumbnd  25055  pntlem3  25098  cusgrasizeindslem1  26002  sspid  26964  ssps  26969  helch  27484  hhssnv  27505  hhsssh  27510  shintcl  27573  chintcl  27575  shlesb1i  27629  omlsi  27647  chlejb1i  27719  chm0i  27733  chabs1  27759  chabs2  27760  spanun  27788  cmidi  27853  pjidmcoi  28420  csmdsymi  28577  sumdmdlem2  28662  dmdbr5ati  28665  mdcompli  28672  dmdcompli  28673  disjdifprg  28770  fcoinver  28798  xppreima  28829  padct  28885  xrinfm  28909  clatp0cl  29002  clatp1cl  29003  xrsmulgzz  29009  xrsp0  29012  xrsp1  29013  gsumle  29110  gsummpt2co  29111  gsumvsca1  29113  gsumvsca2  29114  mdetpmtr1  29217  reff  29234  locfinreflem  29235  pnfneige0  29325  esumsnf  29453  esumcvg  29475  pwsiga  29520  sigagenid  29541  baselcarsg  29695  bnj1253  30339  cvmlift2lem6  30544  mrsubrn  30664  mrsubff1  30665  mrsub0  30667  mrsubccat  30669  mrsubcn  30670  elmrsubrn  30671  elmsubrn  30679  msubrn  30680  msubff1  30707  mthmpps  30733  trpredtr  30974  trpredpo  30979  wzel  31015  wzelOLD  31016  frrlem5c  31030  frrlem10  31035  imagesset  31230  ivthALT  31500  fness  31514  fneref  31515  refssfne  31523  fnemeet1  31531  fnejoin2  31534  filnetlem2  31544  filnetlem4  31546  ontgval  31600  knoppcnlem10  31662  knoppcnlem11  31663  knoppndvlem6  31678  knoppndv  31695  bj-rabtr  32118  bj-rabtrALTALT  32120  bj-rabtrAUTO  32121  bj-restsnid  32221  bj-restpw  32226  bj-restb  32228  bj-resta  32230  bj-restuni2  32232  elxp8  32395  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfposadd  32627  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anc  32663  ftc2nc  32664  areacirclem2  32671  areacirclem3  32672  areacirclem4  32673  areacirc  32675  welb  32701  caures  32726  constcncf  32728  idcncf  32729  sub1cncf  32730  sub2cncf  32731  cnresima  32733  rngoidl  32993  atpsubN  34057  pol1N  34214  1psubclN  34248  cdlemefrs32fva  34706  dia2dimlem13  35383  dibord  35466  dochvalr  35664  hdmapevec  36145  ismrcd1  36279  ismrc  36282  incssnn0  36292  mzpclall  36308  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  aomclem6  36647  kelac1  36651  gicabl  36687  rgspnid  36761  itgpowd  36819  arearect  36820  areaquad  36821  clcnvlem  36949  cnvtrucl0  36950  cnvtrcl0  36952  fvilbd  37000  relexp0a  37027  brfvrtrcld  37045  corcltrcl  37050  clsk3nimkb  37358  clsk1indlem2  37360  ntrclskb  37387  k0004ss2  37470  wnefimgd  37480  wfximgfd  37485  extoimad  37486  funfvima2d  37491  nzss  37538  lhe4.4ex1a  37550  dvsconst  37551  dvsid  37552  dvsef  37553  dvconstbi  37555  binomcxplemnn0  37570  onfrALTlem3  37780  onfrALTlem3VD  38145  cnopn  38233  unisn0  38247  ssinc  38292  ssdec  38293  founiiun  38355  founiiun0  38372  choicefi  38387  evthiccabs  38565  islptre  38686  climconstmpt  38725  fnlimfvre  38741  cncfshift  38759  addccncf2  38761  fsumcncf  38763  cncfperiod  38764  negcncfg  38766  cncfcompt  38768  ioccncflimc  38771  cncfuni  38772  icccncfext  38773  cncficcgt0  38774  icocncflimc  38775  cncfiooicclem1  38779  cncfiooicc  38780  cncfiooiccre  38781  cxpcncf2  38786  fprodcncf  38787  add1cncf  38788  add2cncf  38789  sub1cncfd  38790  sub2cncfd  38791  dvcosre  38799  dvcnre  38804  fperdvper  38808  dvmptresicc  38809  dvmptfprod  38835  itgsinexplem1  38845  itgcoscmulx  38861  ibliooicc  38863  itgsincmulx  38866  itgsubsticclem  38867  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem16  39016  fourierdlem18  39018  fourierdlem21  39021  fourierdlem22  39022  fourierdlem23  39023  fourierdlem32  39032  fourierdlem33  39033  fourierdlem39  39039  fourierdlem40  39040  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem62  39061  fourierdlem68  39067  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem93  39092  fourierdlem94  39093  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  fouriercn  39125  etransclem18  39145  etransclem22  39149  etransclem34  39161  etransclem46  39173  etransclem47  39174  sge0fsum  39280  meaiininclem  39376  hoidmvlelem2  39486  hspdifhsp  39506  hspmbllem2  39517  hspmbl  39519  iinhoiicclem  39564  pimgtmnf2  39601  funresfunco  39854  uhgrsubgrself  40504  uhgrspansubgr  40515  nbupgr  40566  nbumgrvtx  40568  nbgr2vtx1edg  40572  cusgrexi  40662  1wlkvtxeledglem  40827  umgr2adedgwlk  41152  umgr2adedgwlkon  41153  umgr2adedgspth  41155  upgr11wlkdlem2  41313  1pthon2ve  41321  submgmid  41583  rnghmsscmap2  41765  rhmsscmap2  41811  srhmsubc  41868  fldhmsubc  41876  srhmsubcALTV  41887  fldhmsubcALTV  41895  elbigolo1  42149
  Copyright terms: Public domain W3C validator