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

Theorem ssid 3657
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 3640 1 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqimssi  3692  eqimss2i  3693  nsspssun  3890  difid  3981  inv1  4003  disjpss  4061  pwidg  4206  elssuni  4499  unimax  4505  intmin  4529  rintn0  4651  sseliALT  4824  xpss1  5161  xpss2  5162  residm  5465  resdm  5476  resmpt3  5485  ssrnres  5607  ordunidif  5811  dffn3  6092  fdmrn  6102  fvreseq1  6358  fimacnv  6387  iunpw  7020  onsucuni  7070  tfisi  7100  fparlem3  7324  fparlem4  7325  funsssuppss  7366  suppofss1d  7377  suppofss2d  7378  tfrlem1  7517  tz7.48-2  7582  oaordi  7671  omwordi  7696  omass  7705  nnaordi  7743  nnmwordi  7760  fpmg  7925  ralxpmap  7949  boxcutc  7993  domss2  8160  0fin  8229  en1eqsn  8231  findcard2d  8243  fimax2g  8247  domunfican  8274  pwfi  8302  fissuni  8312  fipreima  8313  fsuppmptif  8346  fsuppco2  8349  fsuppcor  8350  mapfienlem1  8351  mapfienlem2  8352  fimin2g  8444  wofib  8491  wemapso  8497  noinfep  8595  cantnfval2  8604  cantnfp1lem3  8615  cantnflem1  8624  tcidm  8660  tc0  8661  r1rankidb  8705  r1pw  8746  rankr1id  8763  scott0  8787  htalem  8797  xpomen  8876  infpwfien  8923  alephsmo  8963  dfac12lem3  9005  ackbij2lem4  9102  cflem  9106  cflecard  9113  cflim2  9123  cfslb  9126  fin4en1  9169  fin23lem13  9192  fin23lem15  9194  fin23lem36  9208  isf32lem1  9213  fin67  9255  dcomex  9307  zorn2lem4  9359  alephexp2  9441  fpwwe2lem13  9502  canthnumlem  9508  wunex2  9598  wuncidm  9606  eltsk2g  9611  axgroth6  9688  axgroth3  9691  xrsup  12707  expcl  12918  hashcard  13184  hashf1lem2  13278  xptrrel  13765  cotrtrclfv  13797  rtrclreclem1  13842  rtrclreclem2  13843  lo1eq  14343  rlimeq  14344  serclim0  14352  isercolllem2  14440  isercoll  14442  summolem3  14489  isum  14494  fsumser  14505  fsumcl  14508  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  flo1  14630  prodmolem3  14707  iprod  14712  iprodn0  14714  fprodss  14722  fprodcl  14726  fprod2d  14755  fprodclf  14767  risefaccl  14790  fallfaccl  14791  eflt  14891  rpnnen2lem3  14989  rpnnen2lem5  14991  rpnnen2lem11  14997  rpnnen2lem12  14998  rexpen  15001  eulerthlem2  15534  ressid  15982  ressinbas  15983  mremre  16311  catsubcat  16546  yon11  16951  yon12  16952  yon2  16953  yonpropd  16955  oppcyon  16956  yonffth  16971  oduclatb  17191  ipopos  17207  fpwipodrs  17211  submid  17398  mulgnncl  17603  mulgnnclOLD  17604  mulgnn0cl  17605  mulgcl  17606  subgid  17643  ghmghmrn  17726  cntrnsg  17820  symggen  17936  sylow3lem5  18092  lsmss1  18125  lsmss2  18127  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumadd  18369  gsumzmhm  18383  gsumzoppg  18390  gsum2dlem1  18415  gsum2dlem2  18416  gsum2d  18417  dprdfinv  18464  dprdf1  18478  dmdprdsplitlem  18482  dprd2db  18488  dpjidcl  18503  ablfac1eulem  18517  ablfac1eu  18518  ablfaclem2  18531  gsumdixp  18655  subrgid  18830  lcomfsupp  18951  lss1  18987  lbsextlem1  19206  rlmval2  19242  rlmbas  19243  rlmplusg  19244  rlm0  19245  rlmmulr  19247  rlmsca  19248  rlmsca2  19249  rlmvsca  19250  rlmtopn  19251  rlmds  19252  psrass1lem  19425  mplsubglem  19482  mpllsslem  19483  mplsubrglem  19487  mplcoe1  19513  mplcoe5  19516  mplbas2  19518  evlslem4  19556  psrbagev1  19558  evlslem2  19560  znf1o  19948  zntoslem  19953  regsumsupp  20016  css0  20081  uvcresum  20180  frlmsslsp  20183  frlmlbs  20184  frlmup1  20185  mamures  20244  mdetrsca2  20458  mdetrlin2  20461  mdetunilem5  20470  mdetunilem9  20474  smadiadetglem1  20525  smadiadetglem2  20526  pmatcollpw3  20637  cpmadumatpolylem2  20735  topopn  20759  fiinbas  20804  topbas  20824  topcld  20887  clstop  20921  ntrtop  20922  opnneissb  20966  opnssneib  20967  opnneiid  20978  neiptopuni  20982  neiptoptop  20983  maxlp  20999  isperf2  21004  restopn2  21029  restperf  21036  idcn  21109  cnconst2  21135  lmres  21152  rncmp  21247  fiuncmp  21255  cmpfi  21259  conncn  21277  1stcelcls  21312  llyidm  21339  nllyidm  21340  toplly  21341  ssref  21363  refref  21364  kgentopon  21389  kgencn2  21408  ptpjpre1  21422  ptbasfi  21432  ptcld  21464  xkopt  21506  elqtop2  21552  qtopuni  21553  ptcmpfi  21664  fbssfi  21688  opnfbas  21693  filtop  21706  isfil2  21707  isfild  21709  fsubbas  21718  ssfg  21723  filssufilg  21762  ufileu  21770  imaelfm  21802  rnelfm  21804  fmfnfmlem4  21808  neiflim  21825  supnfcls  21871  fclscf  21876  flimfnfcls  21879  tsmsfbas  21978  utopbas  22086  xpsxmet  22232  xpsdsval  22233  xpsmet  22234  tmsxms  22338  tmsms  22339  imasf1oxms  22341  imasf1oms  22342  prdsxms  22382  prdsms  22383  tmsxpsval  22390  retopbas  22611  cnngp  22630  cnopn  22637  cnperf  22670  retopconn  22679  fsumcn  22720  abscncf  22751  recncf  22752  imcncf  22753  cjcncf  22754  mulc1cncf  22755  cncfcn1  22760  cncfmpt2f  22764  cncfmpt2ss  22765  addccncf  22766  cdivcncf  22767  negcncf  22768  negfcncf  22769  abscncfALT  22770  cnmpt2pc  22774  xrhmeo  22792  oprpiece1res1  22797  oprpiece1res2  22798  cnrehmeo  22799  iscau3  23122  caubl  23152  caublcls  23153  rrxcph  23226  rrxmval  23234  rrxdstprj1  23238  evthicc2  23275  ovolre  23339  volsuplem  23369  uniiccdif  23392  uniioovol  23393  uniiccvol  23394  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  dyadmbllem  23413  volcn  23420  volivth  23421  itgfsum  23638  iblabslem  23639  iblabs  23640  bddmulibl  23650  cnlimc  23697  cnlimci  23698  dvres3  23722  dvres3a  23723  dvidlem  23724  dvcnp2  23728  dvcn  23729  dvnadd  23737  dvnres  23739  cpnord  23743  cpnres  23745  dvaddbr  23746  dvmulbr  23747  dvcmul  23752  dvcmulf  23753  dvcobr  23754  dvcjbr  23757  dvrec  23763  dvmptntr  23779  dvmptfsum  23783  dveflem  23787  dvef  23788  rolle  23798  dvlipcn  23802  c1liplem1  23804  dvgt0lem2  23811  dvivth  23818  lhop1lem  23821  dvfsumabs  23831  ftc1a  23845  ftc1cn  23851  ftc2  23852  deg1mul3le  23921  plyssc  24001  plyeq0  24012  coeeulem  24025  0dgr  24046  coemulc  24056  coe0  24057  coesub  24058  coe1termlem  24059  dgrmulc  24072  dgrsub  24073  dgrcolem1  24074  dgrcolem2  24075  dvnply2  24087  plycpn  24089  plyremlem  24104  fta1lem  24107  vieta1lem2  24111  aalioulem3  24134  dvntaylp  24170  taylthlem1  24172  taylthlem2  24173  ulmcn  24198  psercn  24225  pserdv  24228  abelth  24240  efcn  24242  efcvx  24248  pige3  24314  dvrelog  24428  logcn  24438  dvloglem  24439  dvlog  24442  dvlog2  24444  efopnlem2  24448  logccv  24454  cxpcn  24531  cxpcn2  24532  cxpcn3  24534  resqrtcn  24535  sqrtcn  24536  loglesqrt  24544  atancn  24708  rlimcnp3  24739  jensen  24760  lgamgulmlem2  24801  ftalem3  24846  basellem2  24853  dchrfi  25025  dchrisumlema  25222  pntrsumo1  25299  pntrsumbnd  25300  pntlem3  25343  uhgrsubgrself  26217  uhgrspansubgr  26228  nbupgr  26285  nbumgrvtx  26287  nbgr2vtx1edg  26291  cusgrexilem2  26394  ifpsnprss  26574  umgr2adedgwlk  26910  umgr2adedgwlkon  26911  umgr2adedgspth  26913  upgr1wlkdlem2  27124  1pthon2ve  27132  sspid  27708  ssps  27713  helch  28228  hhssnv  28249  hhsssh  28254  shintcl  28317  chintcl  28319  shlesb1i  28373  omlsi  28391  chlejb1i  28463  chm0i  28477  chabs1  28503  chabs2  28504  spanun  28532  cmidi  28597  pjidmcoi  29164  csmdsymi  29321  sumdmdlem2  29406  dmdbr5ati  29409  mdcompli  29416  dmdcompli  29417  disjdifprg  29514  fcoinver  29544  xppreima  29577  padct  29625  xrinfm  29647  clatp0cl  29799  clatp1cl  29800  xrsmulgzz  29806  xrsp0  29809  xrsp1  29810  gsumle  29907  gsummpt2co  29908  gsumvsca1  29910  gsumvsca2  29911  mdetpmtr1  30017  reff  30034  locfinreflem  30035  pnfneige0  30125  esumsnf  30254  esumcvg  30276  pwsiga  30321  sigagenid  30342  baselcarsg  30496  iblidicc  30798  cxpcncf1  30801  efmul2picn  30802  fdvposlt  30805  fdvneggt  30806  fdvposle  30807  fdvnegge  30808  reprfz1  30830  breprexplemc  30838  circlemeth  30846  circlevma  30848  circlemethhgt  30849  logdivsqrle  30856  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  bnj1253  31211  cvmlift2lem6  31416  mrsubrn  31536  mrsubff1  31537  mrsub0  31539  mrsubccat  31541  mrsubcn  31542  elmrsubrn  31543  elmsubrn  31551  msubrn  31552  msubff1  31579  mthmpps  31605  trpredtr  31854  trpredpo  31859  wzel  31894  frrlem5c  31911  frrlem10  31916  nosupbnd1lem1  31979  imagesset  32185  ivthALT  32455  fness  32469  fneref  32470  refssfne  32478  fnemeet1  32486  fnejoin2  32489  filnetlem2  32499  filnetlem4  32501  ontgval  32555  knoppcnlem10  32617  knoppcnlem11  32618  knoppndvlem6  32633  knoppndv  32650  bj-rabtr  33051  bj-rabtrALTALT  33053  bj-rabtrAUTO  33054  bj-disj2r  33138  bj-restsnid  33165  bj-restpw  33170  bj-restb  33172  bj-resta  33174  bj-restuni2  33176  elxp8  33349  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfposadd  33587  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anc  33623  ftc2nc  33624  areacirclem2  33631  areacirclem3  33632  areacirclem4  33633  areacirc  33635  welb  33661  caures  33686  constcncf  33688  idcncf  33689  sub1cncf  33690  sub2cncf  33691  cnresima  33693  rngoidl  33953  inxpssres  34217  brssrid  34392  brcnvssrid  34397  refrelid  34411  atpsubN  35357  pol1N  35514  1psubclN  35548  cdlemefrs32fva  36005  dia2dimlem13  36682  dibord  36765  dochvalr  36963  hdmapevec  37444  ismrcd1  37578  ismrc  37581  incssnn0  37591  mzpclall  37607  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  expdioph  37907  aomclem6  37946  kelac1  37950  gicabl  37986  rgspnid  38059  itgpowd  38117  arearect  38118  areaquad  38119  clcnvlem  38247  cnvtrucl0  38248  cnvtrcl0  38250  fvilbd  38298  relexp0a  38325  brfvrtrcld  38343  corcltrcl  38348  clsk3nimkb  38655  clsk1indlem2  38657  ntrclskb  38684  k0004ss2  38767  wnefimgd  38777  wfximgfd  38780  extoimad  38781  funfvima2d  38786  nzss  38833  lhe4.4ex1a  38845  dvsconst  38846  dvsid  38847  dvsef  38848  dvconstbi  38850  binomcxplemnn0  38865  onfrALTlem3  39076  onfrALTlem3VD  39437  unisn0  39536  ssinc  39578  ssdec  39579  founiiun  39674  founiiun0  39691  choicefi  39706  evthiccabs  40036  islptre  40169  climconstmpt  40208  fnlimfvre  40224  cncfshift  40405  addccncf2  40407  fsumcncf  40409  cncfperiod  40410  negcncfg  40412  cncfcompt  40414  ioccncflimc  40416  cncfuni  40417  icccncfext  40418  cncficcgt0  40419  icocncflimc  40420  cncfiooicclem1  40424  cncfiooicc  40425  cncfiooiccre  40426  cxpcncf2  40431  fprodcncf  40432  add1cncf  40433  add2cncf  40434  sub1cncfd  40435  sub2cncfd  40436  dvcosre  40444  dvcnre  40448  fperdvper  40451  dvmptresicc  40452  dvmptfprod  40478  itgsinexplem1  40487  itgcoscmulx  40503  ibliooicc  40505  itgsincmulx  40508  itgsubsticclem  40509  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem16  40658  fourierdlem18  40660  fourierdlem21  40663  fourierdlem22  40664  fourierdlem23  40665  fourierdlem32  40674  fourierdlem33  40675  fourierdlem39  40681  fourierdlem40  40682  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem62  40703  fourierdlem68  40709  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem83  40724  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem93  40734  fourierdlem94  40735  fourierdlem95  40736  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  fouriercn  40767  etransclem18  40787  etransclem22  40791  etransclem34  40803  etransclem46  40815  etransclem47  40816  sge0fsum  40922  meaiininclem  41021  hoidmvlelem2  41131  hspdifhsp  41151  hspmbllem2  41162  hspmbl  41164  iinhoiicclem  41208  pimgtmnf2  41245  smflimsuplem1  41347  smflimsuplem6  41352  funresfunco  41526  submgmid  42118  rnghmsscmap2  42298  rhmsscmap2  42344  srhmsubc  42401  fldhmsubc  42409  srhmsubcALTV  42419  fldhmsubcALTV  42427  elbigolo1  42676
  Copyright terms: Public domain W3C validator