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

Theorem ssid 3210
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 3197 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  eqimssi  3245  eqimss2i  3246  nsspssun  3415  inv1  3494  disjpss  3518  difid  3535  pwidg  3650  elssuni  3871  unimax  3877  intmin  3898  rintn0  4008  ordunidif  4456  iunpw  4586  onsucuni  4635  tfisi  4665  xpss1  4811  xpss2  4812  residm  5002  resdm  5009  resmpt3  5017  ssrnres  5132  dffn3  5412  fimacnv  5673  fparlem3  6236  fparlem4  6237  tfrlem1  6407  tz7.48-2  6470  abianfp  6487  oaordi  6560  omwordi  6585  omass  6594  nnaordi  6632  nnmwordi  6649  fpmg  6809  boxcutc  6875  domss2  7036  0fin  7103  en1eqsn  7104  fimax2g  7119  domunfican  7145  pwfi  7167  fissuni  7176  fipreima  7177  wofib  7276  wemapso  7282  sucprcreg  7329  noinfep  7376  noinfepOLD  7377  cantnfval2  7386  cantnfp1lem3  7398  tcidm  7447  tc0  7448  r1rankidb  7492  r1pw  7533  rankr1id  7550  scott0  7572  htalem  7582  xpomen  7659  infpwfien  7705  alephsmo  7745  dfac12lem3  7787  ackbij2lem4  7884  cflem  7888  cflecard  7895  cflim2  7905  cfslb  7908  fin4en1  7951  fin23lem13  7974  fin23lem15  7976  fin23lem36  7990  isf32lem1  7995  fin67  8037  dcomex  8089  zorn2lem4  8142  alephexp2  8219  fpwwe2lem13  8280  canthnumlem  8286  wunex2  8376  wuncidm  8384  eltsk2g  8389  axgroth6  8466  axgroth3  8469  xrsup  10988  expcl  11137  hashcard  11365  hashf1lem2  11410  lo1eq  12058  rlimeq  12059  serclim0  12067  isercolllem2  12155  isercoll  12157  summolem3  12203  isum  12208  fsumser  12219  fsumcl  12222  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  flo1  12329  eflt  12413  xpnnenOLD  12504  rpnnen2lem3  12511  rpnnen2lem5  12513  rpnnen2lem11  12519  rpnnen2  12520  rexpen  12522  eulerthlem2  12866  ressid  13219  ressinbas  13220  mremre  13522  yon11  14054  yon12  14055  yon2  14056  yonpropd  14058  oppcyon  14059  yonffth  14074  p0le  14165  ple1  14166  oduclatb  14264  ipopos  14279  fpwipodrs  14283  submid  14444  mulgnncl  14598  mulgnn0cl  14599  mulgcl  14600  subgid  14639  cntrnsg  14833  sylow3lem5  14958  lsmss1  14991  lsmss2  14993  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumadd  15221  gsumzsplit  15222  gsumzmhm  15226  gsumzoppg  15232  gsumzinv  15233  gsumsub  15235  gsum2d  15239  dprdfinv  15270  dprdf1  15284  dmdprdsplitlem  15288  dprd2db  15294  dpjidcl  15309  ablfac1eulem  15323  ablfac1eu  15324  ablfaclem2  15337  gsumdixp  15408  subrgid  15563  lss1  15712  lbsextlem1  15927  rlmbas  15964  rlmplusg  15965  rlm0  15966  rlmmulr  15967  rlmsca  15968  rlmsca2  15969  rlmvsca  15970  rlmtopn  15971  rlmds  15972  psrass1lem  16139  mplsubglem  16195  mpllsslem  16196  mplsubrglem  16199  mplcoe1  16225  mplbas2  16228  evlslem4  16261  psrbagev1  16263  evlslem2  16265  znf1o  16521  zntoslem  16526  css0  16605  topopn  16668  fiinbas  16706  topbas  16726  topcld  16788  clstop  16822  ntrtop  16823  opnneissb  16867  opnssneib  16868  opnneiid  16879  maxlp  16894  isperf2  16899  restopn2  16924  restperf  16930  idcn  17003  cnconst2  17027  lmres  17044  rncmp  17139  fiuncmp  17147  cmpfi  17151  concn  17168  1stcelcls  17203  llyidm  17230  nllyidm  17231  toplly  17232  kgentopon  17249  kgencn2  17268  ptpjpre1  17282  ptbasfi  17292  ptcld  17323  xkopt  17365  elqtop2  17408  qtopuni  17409  ptcmpfi  17520  fbssfi  17548  opnfbas  17553  filtop  17566  isfil2  17567  isfild  17569  fsubbas  17578  ssfg  17583  filssufilg  17622  ufileu  17630  imaelfm  17662  rnelfm  17664  fmfnfmlem4  17668  neiflim  17685  supnfcls  17731  fclscf  17736  flimfnfcls  17739  tsmsfbas  17826  xpsxmet  17960  xpsdsval  17961  xpsmet  17962  tmsxms  18048  tmsms  18049  imasf1oxms  18051  imasf1oms  18052  prdsxms  18092  prdsms  18093  tmsxpsval  18100  retopbas  18285  cnngp  18305  cnperf  18341  retopcon  18350  fsumcn  18390  abscncf  18421  recncf  18422  imcncf  18423  cjcncf  18424  mulc1cncf  18425  cncfcn1  18430  cncfmpt2f  18434  cncfmpt2ss  18435  cdivcncf  18436  negcncf  18437  negfcncf  18438  abscncfALT  18439  cnmpt2pc  18442  xrhmeo  18460  oprpiece1res1  18465  oprpiece1res2  18466  cnrehmeo  18467  iscau3  18720  caubl  18749  caublcls  18750  evthicc2  18836  ovolre  18900  volsuplem  18928  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  dyadmbllem  18970  volcn  18977  volivth  18978  itgfsum  19197  iblabslem  19198  iblabs  19199  bddmulibl  19209  cnlimc  19254  cnlimci  19255  dvres3  19279  dvres3a  19280  dvidlem  19281  dvcnp2  19285  dvcn  19286  dvnadd  19294  dvnres  19296  cpnord  19300  cpnres  19302  dvaddbr  19303  dvmulbr  19304  dvcmul  19309  dvcmulf  19310  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvmptntr  19336  dvmptfsum  19338  dveflem  19342  dvef  19343  rolle  19353  dvlipcn  19357  c1liplem1  19359  dvgt0lem2  19366  dvivth  19373  lhop1lem  19376  dvfsumabs  19386  ftc1a  19400  ftc1cn  19406  ftc2  19407  deg1mul3le  19518  plyssc  19598  plyeq0  19609  coeeulem  19622  0dgr  19643  coemulc  19652  coe0  19653  coesub  19654  coe1termlem  19655  dgrmulc  19668  dgrsub  19669  dgrcolem1  19670  dgrcolem2  19671  dvnply2  19683  plycpn  19685  plyremlem  19700  fta1lem  19703  vieta1lem2  19707  aalioulem3  19730  dvntaylp  19766  taylthlem1  19768  taylthlem2  19769  ulmcn  19792  psercn  19818  pserdv  19821  abelth  19833  efcn  19835  efcvx  19841  pige3  19901  dvrelog  20000  logcn  20010  dvloglem  20011  dvlog  20014  dvlog2  20016  efopnlem2  20020  logccv  20026  cxpcn  20101  cxpcn2  20102  cxpcn3  20104  resqrcn  20105  sqrcn  20106  loglesqr  20114  atancn  20248  rlimcnp3  20278  jensen  20299  ftalem3  20328  basellem2  20335  dchrfi  20510  dchrisumlema  20653  pntrsumo1  20730  pntrsumbnd  20731  pntlem3  20774  efghgrp  21056  sspid  21317  ssps  21322  helch  21839  hhssnv  21857  hhsssh  21862  shintcl  21925  chintcl  21927  shlesb1i  21981  omlsi  21999  chlejb1i  22071  chm0i  22085  chabs1  22111  chabs2  22112  spanun  22140  cmidi  22205  pjidmcoi  22773  csmdsymi  22930  sumdmdlem2  23015  dmdbr5ati  23018  mdcompli  23025  dmdcompli  23026  fdmrn  23051  xppreima  23226  xrsmulgzz  23322  disjdifprg  23367  pnfneige0  23389  esumsn  23452  esumcvg  23469  pwsiga  23506  difelsiga  23509  sigagenid  23526  measiuns  23559  dya2iocseg  23594  cvmlift2lem6  23854  relexpdm  24047  relexprn  24048  rtrclreclem.refl  24056  rtrclreclem.subset  24057  prodmolem3  24156  iprod  24161  iprodn0  24163  trpredtr  24304  trpredpo  24309  frrlem5c  24358  frrlem10  24363  ontgval  24942  ovoliunnfl  25001  ftc1cnnclem  25024  ftc1cnnc  25025  areacirclem3  25029  areacirclem4  25030  areacirclem1  25031  areacirclem5  25032  residcp  25180  prl2  25272  inpc  25380  inposet  25381  dominc  25383  rninc  25384  domncnt  25385  ranncnt  25386  dfps2  25392  toplat  25393  fsumprd  25432  clfsebs  25450  fincmpzer  25453  fprodadd  25455  fprodneg  25481  fprodsub  25482  caytr  25503  osneisi  25634  0alg  25859  catsbc  25952  tareltsuc  26001  prismorcsetlem  26015  prismorcset  26017  segline  26244  bsstrs  26249  segray  26258  rayline  26259  ivthALT  26361  fness  26385  ssref  26386  fneref  26387  refref  26388  refssfne  26397  fnemeet1  26418  fnejoin2  26421  filnetlem2  26431  filnetlem4  26433  welb  26520  caures  26579  constcncf  26581  addccncf  26582  idcncf  26583  sub1cncf  26584  sub2cncf  26585  cnresima  26587  rngoidl  26752  ralxpmap  26864  lcomfsup  26871  ismrcd1  26876  ismrc  26879  incssnn0  26889  mzpclall  26908  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  aomclem6  27259  kelac1  27264  frlmsslsp  27351  frlmlbs  27352  frlmup1  27353  gicabl  27366  rgspnid  27480  symggen  27514  lhe4.4ex1a  27649  dvsconst  27650  dvsid  27651  dvsef  27652  dvconstbi  27654  dvcosre  27844  itgsinexplem1  27851  funresfunco  28093  onfrALTlem3  28608  onfrALTlem3VD  28979  bnj1253  29363  atpsubN  30564  pol1N  30721  1psubclN  30755  cdlemefrs32fva  31211  dia2dimlem13  31888  dibord  31971  dochvalr  32169  hdmapevec  32650
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator