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

Theorem ssid 3363
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
ssid  |-  A  C_  A

Proof of Theorem ssid
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 id 22 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3348 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  eqimssi  3398  eqimss2i  3399  nsspssun  3571  inv1  3652  disjpss  3717  difid  3735  pwidg  3861  elssuni  4109  unimax  4115  intmin  4136  rintn0  4249  sseliALT  4411  ordunidif  4754  xpss1  4935  xpss2  4936  residm  5129  resdm  5136  resmpt3  5145  ssrnres  5264  dffn3  5554  fdmrn  5561  fvreseq1  5792  fimacnv  5823  iunpw  6379  onsucuni  6428  tfisi  6458  fparlem3  6663  fparlem4  6664  funsssuppss  6704  suppofss1d  6715  suppofss2d  6716  tfrlem1  6821  tz7.48-2  6883  abianfp  6900  oaordi  6973  omwordi  6998  omass  7007  nnaordi  7045  nnmwordi  7062  fpmg  7226  ralxpmap  7250  boxcutc  7294  domss2  7458  0fin  7528  en1eqsn  7530  findcard2d  7542  fimax2g  7546  domunfican  7572  pwfi  7594  fissuni  7604  fipreima  7605  fsuppmptif  7637  fsuppco2  7640  fsuppcor  7641  mapfienlem1  7642  mapfienlem2  7643  wofib  7747  wemapso  7753  sucprcregOLD  7803  noinfep  7853  noinfepOLD  7854  cantnfval2  7865  cantnfp1lem3  7876  cantnflem1d  7884  cantnflem1  7885  cantnfval2OLD  7895  cantnfp1lem3OLD  7902  tcidm  7954  tc0  7955  r1rankidb  7999  r1pw  8040  rankr1id  8057  scott0  8081  htalem  8091  xpomen  8170  infpwfien  8220  alephsmo  8260  dfac12lem3  8302  ackbij2lem4  8399  cflem  8403  cflecard  8410  cflim2  8420  cfslb  8423  fin4en1  8466  fin23lem13  8489  fin23lem15  8491  fin23lem36  8505  isf32lem1  8510  fin67  8552  dcomex  8604  zorn2lem4  8656  alephexp2  8733  fpwwe2lem13  8796  canthnumlem  8802  wunex2  8892  wuncidm  8900  eltsk2g  8905  axgroth6  8982  axgroth3  8985  xrsup  11690  expcl  11866  hashcard  12108  hashf1lem2  12192  lo1eq  13029  rlimeq  13030  serclim0  13038  isercolllem2  13126  isercoll  13128  summolem3  13174  isum  13179  fsumser  13190  fsumcl  13193  fsum2d  13221  fsumabs  13246  fsumrlim  13256  fsumo1  13257  fsumiun  13266  flo1  13299  eflt  13383  xpnnenOLD  13474  rpnnen2lem3  13481  rpnnen2lem5  13483  rpnnen2lem11  13489  rpnnen2  13490  rexpen  13492  eulerthlem2  13839  ressid  14215  ressinbas  14216  mremre  14524  yon11  15056  yon12  15057  yon2  15058  yonpropd  15060  oppcyon  15061  yonffth  15076  oduclatb  15296  ipopos  15312  fpwipodrs  15316  submid  15460  mulgnncl  15621  mulgnn0cl  15622  mulgcl  15623  subgid  15662  cntrnsg  15838  symggen  15955  sylow3lem5  16109  lsmss1  16142  lsmss2  16144  gsumzres  16367  gsumzcl2  16368  gsumzf1o  16370  gsumzresOLD  16371  gsumzclOLD  16372  gsumzf1oOLD  16373  gsumadd  16391  gsumaddOLD  16392  gsumzsplitOLD  16398  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzoppg  16415  gsumzoppgOLD  16416  gsumzinvOLD  16418  gsumsubOLD  16423  gsum2dlem1  16434  gsum2dlem2  16435  gsum2d  16436  gsum2dOLD  16437  dprdfinv  16482  dprdfinvOLD  16489  dprdf1  16503  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dprd2db  16515  dpjidcl  16530  dpjidclOLD  16537  ablfac1eulem  16546  ablfac1eu  16547  ablfaclem2  16560  gsumdixpOLD  16634  gsumdixp  16635  subrgid  16790  lcomfsupOLD  16907  lcomfsupp  16908  lss1  16941  lbsextlem1  17160  rlmval2  17196  rlmbas  17197  rlmplusg  17198  rlm0  17199  rlmmulr  17201  rlmsca  17202  rlmsca2  17203  rlmvsca  17204  rlmtopn  17205  rlmds  17206  psrass1lem  17380  mplsubglem  17443  mpllsslem  17444  mplsubglemOLD  17445  mpllsslemOLD  17446  mplsubrglem  17450  mplsubrglemOLD  17451  mplcoe1  17477  mplbas2  17482  mplbas2OLD  17483  evlslem4OLD  17517  evlslem4  17518  psrbagev1  17521  psrbagev1OLD  17522  evlslem2  17524  ply1coe  17642  znf1o  17825  zntoslem  17830  regsumsupp  17893  css0  17955  frlmip  18044  uvcresum  18059  frlmsslsp  18064  frlmsslspOLD  18065  frlmlbs  18066  frlmup1  18067  mamures  18131  mdetrsca2  18252  mdetrlin2  18254  mdetunilem5  18263  mdetunilem9  18267  smadiadetglem1  18318  smadiadetglem2  18319  topopn  18360  fiinbas  18398  topbas  18418  topcld  18480  clstop  18514  ntrtop  18515  opnneissb  18559  opnssneib  18560  opnneiid  18571  neiptopuni  18575  neiptoptop  18576  maxlp  18592  isperf2  18597  restopn2  18622  restperf  18629  idcn  18702  cnconst2  18728  lmres  18745  rncmp  18840  fiuncmp  18848  cmpfi  18852  concn  18871  1stcelcls  18906  llyidm  18933  nllyidm  18934  toplly  18935  kgentopon  18952  kgencn2  18971  ptpjpre1  18985  ptbasfi  18995  ptcld  19027  xkopt  19069  elqtop2  19115  qtopuni  19116  ptcmpfi  19227  fbssfi  19251  opnfbas  19256  filtop  19269  isfil2  19270  isfild  19272  fsubbas  19281  ssfg  19286  filssufilg  19325  ufileu  19333  imaelfm  19365  rnelfm  19367  fmfnfmlem4  19371  neiflim  19388  supnfcls  19434  fclscf  19439  flimfnfcls  19442  tsmsfbas  19539  utopbas  19651  xpsxmet  19796  xpsdsval  19797  xpsmet  19798  tmsxms  19902  tmsms  19903  imasf1oxms  19905  imasf1oms  19906  prdsxms  19946  prdsms  19947  tmsxpsval  19954  retopbas  20180  cnngp  20200  cnperf  20238  retopcon  20247  fsumcn  20287  abscncf  20318  recncf  20319  imcncf  20320  cjcncf  20321  mulc1cncf  20322  cncfcn1  20327  cncfmpt2f  20331  cncfmpt2ss  20332  addccncf  20333  cdivcncf  20334  negcncf  20335  negfcncf  20336  abscncfALT  20337  cnmpt2pc  20341  xrhmeo  20359  oprpiece1res1  20364  oprpiece1res2  20365  cnrehmeo  20366  iscau3  20630  caubl  20659  caublcls  20660  rrxip  20735  rrxcph  20737  rrxmval  20745  rrxdstprj1  20749  evthicc2  20785  ovolre  20849  volsuplem  20877  uniiccdif  20899  uniioovol  20900  uniiccvol  20901  uniioombllem3  20906  uniioombllem4  20907  uniioombllem5  20908  dyadmbllem  20920  volcn  20927  volivth  20928  itgfsum  21145  iblabslem  21146  iblabs  21147  bddmulibl  21157  cnlimc  21204  cnlimci  21205  dvres3  21229  dvres3a  21230  dvidlem  21231  dvcnp2  21235  dvcn  21236  dvnadd  21244  dvnres  21246  cpnord  21250  cpnres  21252  dvaddbr  21253  dvmulbr  21254  dvcmul  21259  dvcmulf  21260  dvcobr  21261  dvcjbr  21264  dvrec  21270  dvmptntr  21286  dvmptfsum  21288  dveflem  21292  dvef  21293  rolle  21303  dvlipcn  21307  c1liplem1  21309  dvgt0lem2  21316  dvivth  21323  lhop1lem  21326  dvfsumabs  21336  ftc1a  21350  ftc1cn  21356  ftc2  21357  deg1mul3le  21472  plyssc  21552  plyeq0  21563  coeeulem  21576  0dgr  21597  coemulc  21606  coe0  21607  coesub  21608  coe1termlem  21609  dgrmulc  21622  dgrsub  21623  dgrcolem1  21624  dgrcolem2  21625  dvnply2  21637  plycpn  21639  plyremlem  21654  fta1lem  21657  vieta1lem2  21661  aalioulem3  21684  dvntaylp  21720  taylthlem1  21722  taylthlem2  21723  ulmcn  21748  psercn  21775  pserdv  21778  abelth  21790  efcn  21792  efcvx  21798  pige3  21863  dvrelog  21966  logcn  21976  dvloglem  21977  dvlog  21980  dvlog2  21982  efopnlem2  21986  logccv  21992  cxpcn  22067  cxpcn2  22068  cxpcn3  22070  resqrcn  22071  sqrcn  22072  loglesqr  22080  atancn  22215  rlimcnp3  22245  jensen  22266  ftalem3  22296  basellem2  22303  dchrfi  22478  dchrisumlema  22621  pntrsumo1  22698  pntrsumbnd  22699  pntlem3  22742  cusgrasizeindslem2  23204  efghgrp  23682  sspid  23945  ssps  23950  helch  24468  hhssnv  24487  hhsssh  24492  shintcl  24555  chintcl  24557  shlesb1i  24611  omlsi  24629  chlejb1i  24701  chm0i  24715  chabs1  24741  chabs2  24742  spanun  24770  cmidi  24835  pjidmcoi  25403  csmdsymi  25560  sumdmdlem2  25645  dmdbr5ati  25648  mdcompli  25655  dmdcompli  25656  disjdifprg  25742  xppreima  25787  xrinfm  25872  clatp0cl  25954  clatp1cl  25955  xrsmulgzz  25961  xrsp0  25964  xrsp1  25965  gsumle  26097  gsummpt2co  26100  gsumvsca1  26103  gsumvsca2  26104  pnfneige0  26234  esumsn  26368  esumcvg  26388  pwsiga  26426  sigagenid  26447  lgamgulmlem2  26863  cvmlift2lem6  27044  relexpdm  27183  relexprn  27184  rtrclreclem.refl  27192  rtrclreclem.subset  27193  prodmolem3  27292  iprod  27297  iprodn0  27299  fprodss  27307  fprodcl  27311  fprod2d  27338  risefaccl  27364  fallfaccl  27365  trpredtr  27540  trpredpo  27545  wzel  27607  frrlem5c  27620  frrlem10  27625  imagesset  27830  ontgval  28124  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  mbfposadd  28280  ftc1cnnclem  28306  ftc1cnnc  28307  ftc1anc  28316  ftc2nc  28317  areacirclem2  28326  areacirclem3  28327  areacirclem4  28328  areacirc  28330  ivthALT  28371  fness  28395  ssref  28396  fneref  28397  refref  28398  refssfne  28407  fnemeet1  28428  fnejoin2  28431  filnetlem2  28441  filnetlem4  28443  welb  28471  caures  28497  constcncf  28499  idcncf  28500  sub1cncf  28501  sub2cncf  28502  cnresima  28504  rngoidl  28665  ismrcd1  28876  ismrc  28879  incssnn0  28889  mzpclall  28905  rmydioph  29205  rmxdioph  29207  expdiophlem2  29213  expdioph  29214  aomclem6  29254  kelac1  29258  gicabl  29296  rgspnid  29371  itgpowd  29432  arearect  29433  areaquad  29434  lhe4.4ex1a  29445  dvsconst  29446  dvsid  29447  dvsef  29448  dvconstbi  29450  dvcosre  29631  itgsinexplem1  29637  funresfunco  29874  mptscmfsuppd  30630  ply1coefsupp  30631  onfrALTlem3  30950  onfrALTlem3VD  31322  bnj1253  31707  bj-rabtr  32015  bj-rabtrAUTO  32017  atpsubN  32967  pol1N  33124  1psubclN  33158  cdlemefrs32fva  33614  dia2dimlem13  34291  dibord  34374  dochvalr  34572  hdmapevec  35053
  Copyright terms: Public domain W3C validator