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

Theorem ssid 3197
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 19 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3184 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  eqimssi  3232  eqimss2i  3233  nsspssun  3402  inv1  3481  disjpss  3505  difid  3522  pwidg  3637  elssuni  3855  unimax  3861  intmin  3882  rintn0  3992  ordunidif  4440  iunpw  4570  onsucuni  4619  tfisi  4649  xpss1  4795  xpss2  4796  residm  4986  resdm  4993  resmpt3  5001  ssrnres  5116  dffn3  5396  fimacnv  5657  fparlem3  6220  fparlem4  6221  tfrlem1  6391  tz7.48-2  6454  abianfp  6471  oaordi  6544  omwordi  6569  omass  6578  nnaordi  6616  nnmwordi  6633  fpmg  6793  boxcutc  6859  domss2  7020  0fin  7087  en1eqsn  7088  fimax2g  7103  domunfican  7129  pwfi  7151  fissuni  7160  fipreima  7161  wofib  7260  wemapso  7266  sucprcreg  7313  noinfep  7360  noinfepOLD  7361  cantnfval2  7370  cantnfp1lem3  7382  tcidm  7431  tc0  7432  r1rankidb  7476  r1pw  7517  rankr1id  7534  scott0  7556  htalem  7566  xpomen  7643  infpwfien  7689  alephsmo  7729  dfac12lem3  7771  ackbij2lem4  7868  cflem  7872  cflecard  7879  cflim2  7889  cfslb  7892  fin4en1  7935  fin23lem13  7958  fin23lem15  7960  fin23lem36  7974  isf32lem1  7979  fin67  8021  dcomex  8073  zorn2lem4  8126  alephexp2  8203  fpwwe2lem13  8264  canthnumlem  8270  wunex2  8360  wuncidm  8368  eltsk2g  8373  axgroth6  8450  axgroth3  8453  xrsup  10972  expcl  11121  hashcard  11349  hashf1lem2  11394  lo1eq  12042  rlimeq  12043  serclim0  12051  isercolllem2  12139  isercoll  12141  summolem3  12187  isum  12192  fsumser  12203  fsumcl  12206  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  flo1  12313  eflt  12397  xpnnenOLD  12488  rpnnen2lem3  12495  rpnnen2lem5  12497  rpnnen2lem11  12503  rpnnen2  12504  rexpen  12506  eulerthlem2  12850  ressid  13203  ressinbas  13204  mremre  13506  yon11  14038  yon12  14039  yon2  14040  yonpropd  14042  oppcyon  14043  yonffth  14058  p0le  14149  ple1  14150  oduclatb  14248  ipopos  14263  fpwipodrs  14267  submid  14428  mulgnncl  14582  mulgnn0cl  14583  mulgcl  14584  subgid  14623  cntrnsg  14817  sylow3lem5  14942  lsmss1  14975  lsmss2  14977  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumadd  15205  gsumzsplit  15206  gsumzmhm  15210  gsumzoppg  15216  gsumzinv  15217  gsumsub  15219  gsum2d  15223  dprdfinv  15254  dprdf1  15268  dmdprdsplitlem  15272  dprd2db  15278  dpjidcl  15293  ablfac1eulem  15307  ablfac1eu  15308  ablfaclem2  15321  gsumdixp  15392  subrgid  15547  lss1  15696  lbsextlem1  15911  rlmbas  15948  rlmplusg  15949  rlm0  15950  rlmmulr  15951  rlmsca  15952  rlmsca2  15953  rlmvsca  15954  rlmtopn  15955  rlmds  15956  psrass1lem  16123  mplsubglem  16179  mpllsslem  16180  mplsubrglem  16183  mplcoe1  16209  mplbas2  16212  evlslem4  16245  psrbagev1  16247  evlslem2  16249  znf1o  16505  zntoslem  16510  css0  16589  topopn  16652  fiinbas  16690  topbas  16710  topcld  16772  clstop  16806  ntrtop  16807  opnneissb  16851  opnssneib  16852  opnneiid  16863  maxlp  16878  isperf2  16883  restopn2  16908  restperf  16914  idcn  16987  cnconst2  17011  lmres  17028  rncmp  17123  fiuncmp  17131  cmpfi  17135  concn  17152  1stcelcls  17187  llyidm  17214  nllyidm  17215  toplly  17216  kgentopon  17233  kgencn2  17252  ptpjpre1  17266  ptbasfi  17276  ptcld  17307  xkopt  17349  elqtop2  17392  qtopuni  17393  ptcmpfi  17504  fbssfi  17532  opnfbas  17537  filtop  17550  isfil2  17551  isfild  17553  fsubbas  17562  ssfg  17567  filssufilg  17606  ufileu  17614  imaelfm  17646  rnelfm  17648  fmfnfmlem4  17652  neiflim  17669  supnfcls  17715  fclscf  17720  flimfnfcls  17723  tsmsfbas  17810  xpsxmet  17944  xpsdsval  17945  xpsmet  17946  tmsxms  18032  tmsms  18033  imasf1oxms  18035  imasf1oms  18036  prdsxms  18076  prdsms  18077  tmsxpsval  18084  retopbas  18269  cnngp  18289  cnperf  18325  retopcon  18334  fsumcn  18374  abscncf  18405  recncf  18406  imcncf  18407  cjcncf  18408  mulc1cncf  18409  cncfcn1  18414  cncfmpt2f  18418  cncfmpt2ss  18419  cdivcncf  18420  negcncf  18421  negfcncf  18422  abscncfALT  18423  cnmpt2pc  18426  xrhmeo  18444  oprpiece1res1  18449  oprpiece1res2  18450  cnrehmeo  18451  iscau3  18704  caubl  18733  caublcls  18734  evthicc2  18820  ovolre  18884  volsuplem  18912  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  dyadmbllem  18954  volcn  18961  volivth  18962  itgfsum  19181  iblabslem  19182  iblabs  19183  bddmulibl  19193  cnlimc  19238  cnlimci  19239  dvres3  19263  dvres3a  19264  dvidlem  19265  dvcnp2  19269  dvcn  19270  dvnadd  19278  dvnres  19280  cpnord  19284  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvcmul  19293  dvcmulf  19294  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvmptntr  19320  dvmptfsum  19322  dveflem  19326  dvef  19327  rolle  19337  dvlipcn  19341  c1liplem1  19343  dvgt0lem2  19350  dvivth  19357  lhop1lem  19360  dvfsumabs  19370  ftc1a  19384  ftc1cn  19390  ftc2  19391  deg1mul3le  19502  plyssc  19582  plyeq0  19593  coeeulem  19606  0dgr  19627  coemulc  19636  coe0  19637  coesub  19638  coe1termlem  19639  dgrmulc  19652  dgrsub  19653  dgrcolem1  19654  dgrcolem2  19655  dvnply2  19667  plycpn  19669  plyremlem  19684  fta1lem  19687  vieta1lem2  19691  aalioulem3  19714  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  ulmcn  19776  psercn  19802  pserdv  19805  abelth  19817  efcn  19819  efcvx  19825  pige3  19885  dvrelog  19984  logcn  19994  dvloglem  19995  dvlog  19998  dvlog2  20000  efopnlem2  20004  logccv  20010  cxpcn  20085  cxpcn2  20086  cxpcn3  20088  resqrcn  20089  sqrcn  20090  loglesqr  20098  atancn  20232  rlimcnp3  20262  jensen  20283  ftalem3  20312  basellem2  20319  dchrfi  20494  dchrisumlema  20637  pntrsumo1  20714  pntrsumbnd  20715  pntlem3  20758  efghgrp  21040  sspid  21301  ssps  21306  helch  21823  hhssnv  21841  hhsssh  21846  shintcl  21909  chintcl  21911  shlesb1i  21965  omlsi  21983  chlejb1i  22055  chm0i  22069  chabs1  22095  chabs2  22096  spanun  22124  cmidi  22189  pjidmcoi  22757  csmdsymi  22914  sumdmdlem2  22999  dmdbr5ati  23002  mdcompli  23009  dmdcompli  23010  fdmrn  23035  xppreima  23211  xrsmulgzz  23307  disjdifprg  23352  pnfneige0  23374  esumsn  23437  esumcvg  23454  pwsiga  23491  difelsiga  23494  sigagenid  23511  measiuns  23544  dya2iocseg  23579  cvmlift2lem6  23839  relexpdm  24032  relexprn  24033  rtrclreclem.refl  24041  rtrclreclem.subset  24042  trpredtr  24233  trpredpo  24238  frrlem5c  24287  frrlem10  24292  ontgval  24870  areacirclem3  24926  areacirclem4  24927  areacirclem1  24928  areacirclem5  24929  residcp  25077  prl2  25169  inpc  25277  inposet  25278  dominc  25280  rninc  25281  domncnt  25282  ranncnt  25283  dfps2  25289  toplat  25290  fsumprd  25329  clfsebs  25347  fincmpzer  25350  fprodadd  25352  fprodneg  25378  fprodsub  25379  caytr  25400  osneisi  25531  0alg  25756  catsbc  25849  tareltsuc  25898  prismorcsetlem  25912  prismorcset  25914  segline  26141  bsstrs  26146  segray  26155  rayline  26156  ivthALT  26258  fness  26282  ssref  26283  fneref  26284  refref  26285  refssfne  26294  fnemeet1  26315  fnejoin2  26318  filnetlem2  26328  filnetlem4  26330  welb  26417  caures  26476  constcncf  26478  addccncf  26479  idcncf  26480  sub1cncf  26481  sub2cncf  26482  cnresima  26484  rngoidl  26649  ralxpmap  26761  lcomfsup  26768  ismrcd1  26773  ismrc  26776  incssnn0  26786  mzpclall  26805  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  expdioph  27116  aomclem6  27156  kelac1  27161  frlmsslsp  27248  frlmlbs  27249  frlmup1  27250  gicabl  27263  rgspnid  27377  symggen  27411  lhe4.4ex1a  27546  dvsconst  27547  dvsid  27548  dvsef  27549  dvconstbi  27551  dvcosre  27741  itgsinexplem1  27748  funresfunco  27988  onfrALTlem3  28309  onfrALTlem3VD  28663  bnj1253  29047  atpsubN  29942  pol1N  30099  1psubclN  30133  cdlemefrs32fva  30589  dia2dimlem13  31266  dibord  31349  dochvalr  31547  hdmapevec  32028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator