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

Theorem ssid 3335
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 20 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3320 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    C_ wss 3288
This theorem is referenced by:  eqimssi  3370  eqimss2i  3371  nsspssun  3542  inv1  3622  disjpss  3646  difid  3664  pwidg  3779  elssuni  4011  unimax  4017  intmin  4038  rintn0  4149  ordunidif  4597  iunpw  4726  onsucuni  4775  tfisi  4805  xpss1  4951  xpss2  4952  residm  5144  resdm  5151  resmpt3  5159  ssrnres  5276  dffn3  5565  fimacnv  5829  fparlem3  6415  fparlem4  6416  tfrlem1  6603  tz7.48-2  6666  abianfp  6683  oaordi  6756  omwordi  6781  omass  6790  nnaordi  6828  nnmwordi  6845  fpmg  7006  boxcutc  7072  domss2  7233  0fin  7303  en1eqsn  7305  fimax2g  7320  domunfican  7346  pwfi  7368  fissuni  7377  fipreima  7378  wofib  7478  wemapso  7484  sucprcreg  7531  noinfep  7578  noinfepOLD  7579  cantnfval2  7588  cantnfp1lem3  7600  tcidm  7649  tc0  7650  r1rankidb  7694  r1pw  7735  rankr1id  7752  scott0  7774  htalem  7784  xpomen  7861  infpwfien  7907  alephsmo  7947  dfac12lem3  7989  ackbij2lem4  8086  cflem  8090  cflecard  8097  cflim2  8107  cfslb  8110  fin4en1  8153  fin23lem13  8176  fin23lem15  8178  fin23lem36  8192  isf32lem1  8197  fin67  8239  dcomex  8291  zorn2lem4  8343  alephexp2  8420  fpwwe2lem13  8481  canthnumlem  8487  wunex2  8577  wuncidm  8585  eltsk2g  8590  axgroth6  8667  axgroth3  8670  xrsup  11212  expcl  11362  hashcard  11601  hashf1lem2  11668  lo1eq  12325  rlimeq  12326  serclim0  12334  isercolllem2  12422  isercoll  12424  summolem3  12471  isum  12476  fsumser  12487  fsumcl  12490  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  fsumiun  12563  flo1  12597  eflt  12681  xpnnenOLD  12772  rpnnen2lem3  12779  rpnnen2lem5  12781  rpnnen2lem11  12787  rpnnen2  12788  rexpen  12790  eulerthlem2  13134  ressid  13487  ressinbas  13488  mremre  13792  yon11  14324  yon12  14325  yon2  14326  yonpropd  14328  oppcyon  14329  yonffth  14344  p0le  14435  ple1  14436  oduclatb  14534  ipopos  14549  fpwipodrs  14553  submid  14714  mulgnncl  14868  mulgnn0cl  14869  mulgcl  14870  subgid  14909  cntrnsg  15103  sylow3lem5  15228  lsmss1  15261  lsmss2  15263  gsumzres  15480  gsumzcl  15481  gsumzf1o  15482  gsumadd  15491  gsumzsplit  15492  gsumzmhm  15496  gsumzoppg  15502  gsumzinv  15503  gsumsub  15505  gsum2d  15509  dprdfinv  15540  dprdf1  15554  dmdprdsplitlem  15558  dprd2db  15564  dpjidcl  15579  ablfac1eulem  15593  ablfac1eu  15594  ablfaclem2  15607  gsumdixp  15678  subrgid  15833  lss1  15978  lbsextlem1  16193  rlmbas  16230  rlmplusg  16231  rlm0  16232  rlmmulr  16233  rlmsca  16234  rlmsca2  16235  rlmvsca  16236  rlmtopn  16237  rlmds  16238  psrass1lem  16405  mplsubglem  16461  mpllsslem  16462  mplsubrglem  16465  mplcoe1  16491  mplbas2  16494  evlslem4  16527  psrbagev1  16529  evlslem2  16531  znf1o  16795  zntoslem  16800  css0  16879  topopn  16942  fiinbas  16980  topbas  17000  topcld  17062  clstop  17096  ntrtop  17097  opnneissb  17141  opnssneib  17142  opnneiid  17153  neiptopuni  17157  neiptoptop  17158  maxlp  17173  isperf2  17178  restopn2  17203  restperf  17210  idcn  17283  cnconst2  17309  lmres  17326  rncmp  17421  fiuncmp  17429  cmpfi  17433  concn  17450  1stcelcls  17485  llyidm  17512  nllyidm  17513  toplly  17514  kgentopon  17531  kgencn2  17550  ptpjpre1  17564  ptbasfi  17574  ptcld  17606  xkopt  17648  elqtop2  17694  qtopuni  17695  ptcmpfi  17806  fbssfi  17830  opnfbas  17835  filtop  17848  isfil2  17849  isfild  17851  fsubbas  17860  ssfg  17865  filssufilg  17904  ufileu  17912  imaelfm  17944  rnelfm  17946  fmfnfmlem4  17950  neiflim  17967  supnfcls  18013  fclscf  18018  flimfnfcls  18021  tsmsfbas  18118  utopbas  18226  xpsxmet  18371  xpsdsval  18372  xpsmet  18373  tmsxms  18477  tmsms  18478  imasf1oxms  18480  imasf1oms  18481  prdsxms  18521  prdsms  18522  tmsxpsval  18529  retopbas  18755  cnngp  18775  cnperf  18812  retopcon  18821  fsumcn  18861  abscncf  18892  recncf  18893  imcncf  18894  cjcncf  18895  mulc1cncf  18896  cncfcn1  18901  cncfmpt2f  18905  cncfmpt2ss  18906  addccncf  18907  cdivcncf  18908  negcncf  18909  negfcncf  18910  abscncfALT  18911  cnmpt2pc  18914  xrhmeo  18932  oprpiece1res1  18937  oprpiece1res2  18938  cnrehmeo  18939  iscau3  19192  caubl  19221  caublcls  19222  evthicc2  19318  ovolre  19382  volsuplem  19410  uniiccdif  19431  uniioovol  19432  uniiccvol  19433  uniioombllem3  19438  uniioombllem4  19439  uniioombllem5  19440  dyadmbllem  19452  volcn  19459  volivth  19460  itgfsum  19679  iblabslem  19680  iblabs  19681  bddmulibl  19691  cnlimc  19736  cnlimci  19737  dvres3  19761  dvres3a  19762  dvidlem  19763  dvcnp2  19767  dvcn  19768  dvnadd  19776  dvnres  19778  cpnord  19782  cpnres  19784  dvaddbr  19785  dvmulbr  19786  dvcmul  19791  dvcmulf  19792  dvcobr  19793  dvcjbr  19796  dvrec  19802  dvmptntr  19818  dvmptfsum  19820  dveflem  19824  dvef  19825  rolle  19835  dvlipcn  19839  c1liplem1  19841  dvgt0lem2  19848  dvivth  19855  lhop1lem  19858  dvfsumabs  19868  ftc1a  19882  ftc1cn  19888  ftc2  19889  deg1mul3le  20000  plyssc  20080  plyeq0  20091  coeeulem  20104  0dgr  20125  coemulc  20134  coe0  20135  coesub  20136  coe1termlem  20137  dgrmulc  20150  dgrsub  20151  dgrcolem1  20152  dgrcolem2  20153  dvnply2  20165  plycpn  20167  plyremlem  20182  fta1lem  20185  vieta1lem2  20189  aalioulem3  20212  dvntaylp  20248  taylthlem1  20250  taylthlem2  20251  ulmcn  20276  psercn  20303  pserdv  20306  abelth  20318  efcn  20320  efcvx  20326  pige3  20386  dvrelog  20489  logcn  20499  dvloglem  20500  dvlog  20503  dvlog2  20505  efopnlem2  20509  logccv  20515  cxpcn  20590  cxpcn2  20591  cxpcn3  20593  resqrcn  20594  sqrcn  20595  loglesqr  20603  atancn  20737  rlimcnp3  20767  jensen  20788  ftalem3  20818  basellem2  20825  dchrfi  21000  dchrisumlema  21143  pntrsumo1  21220  pntrsumbnd  21221  pntlem3  21264  cusgrasizeindslem2  21444  efghgrp  21922  sspid  22185  ssps  22190  helch  22707  hhssnv  22725  hhsssh  22730  shintcl  22793  chintcl  22795  shlesb1i  22849  omlsi  22867  chlejb1i  22939  chm0i  22953  chabs1  22979  chabs2  22980  spanun  23008  cmidi  23073  pjidmcoi  23641  csmdsymi  23798  sumdmdlem2  23883  dmdbr5ati  23886  mdcompli  23893  dmdcompli  23894  disjdifprg  23978  fdmrn  24000  xppreima  24020  xrinfm  24082  clatp0ex  24154  clatp1ex  24155  xrsmulgzz  24161  xrsp0  24164  xrsp1  24165  pnfneige0  24297  esumsn  24417  esumcvg  24437  pwsiga  24474  sigagenid  24495  lgamgulmlem2  24775  cvmlift2lem6  24956  relexpdm  25096  relexprn  25097  rtrclreclem.refl  25105  rtrclreclem.subset  25106  prodmolem3  25220  iprod  25225  iprodn0  25227  fprodss  25235  fprodcl  25239  fprod2d  25266  risefaccl  25291  fallfaccl  25292  trpredtr  25455  trpredpo  25460  frrlem5c  25509  frrlem10  25514  ontgval  26093  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  ovoliunnfl  26155  voliunnfl  26157  volsupnfl  26158  mbfposadd  26161  ftc1cnnclem  26185  ftc1cnnc  26186  areacirclem3  26190  areacirclem4  26191  areacirclem1  26192  areacirclem5  26193  ivthALT  26236  fness  26260  ssref  26261  fneref  26262  refref  26263  refssfne  26272  fnemeet1  26293  fnejoin2  26296  filnetlem2  26306  filnetlem4  26308  welb  26336  caures  26364  constcncf  26366  idcncf  26367  sub1cncf  26368  sub2cncf  26369  cnresima  26371  rngoidl  26532  ralxpmap  26640  lcomfsup  26645  ismrcd1  26650  ismrc  26653  incssnn0  26663  mzpclall  26682  rmydioph  26983  rmxdioph  26985  expdiophlem2  26991  expdioph  26992  aomclem6  27032  kelac1  27037  frlmsslsp  27124  frlmlbs  27125  frlmup1  27126  gicabl  27139  rgspnid  27253  symggen  27287  lhe4.4ex1a  27422  dvsconst  27423  dvsid  27424  dvsef  27425  dvconstbi  27427  dvcosre  27616  itgsinexplem1  27623  funresfunco  27864  onfrALTlem3  28349  onfrALTlem3VD  28717  bnj1253  29104  atpsubN  30247  pol1N  30404  1psubclN  30438  cdlemefrs32fva  30894  dia2dimlem13  31571  dibord  31654  dochvalr  31852  hdmapevec  32333
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator