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

Theorem ssid 3172
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
StepHypRef Expression
1 id 21 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3159 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3127
This theorem is referenced by:  eqimssi  3207  eqimss2i  3208  nsspssun  3377  inv1  3456  disjpss  3480  difid  3497  pwidg  3611  elssuni  3829  unimax  3835  intmin  3856  rintn0  3966  ordunidif  4412  iunpw  4542  onsucuni  4591  tfisi  4621  xpss1  4783  xpss2  4784  residm  4974  resdm  4981  resmpt3  4989  ssrnres  5104  dffn3  5334  fimacnv  5591  fparlem3  6154  fparlem4  6155  tfrlem1  6359  tz7.48-2  6422  abianfp  6439  oaordi  6512  omwordi  6537  omass  6546  nnaordi  6584  nnmwordi  6601  fpmg  6761  boxcutc  6827  domss2  6988  0fin  7055  en1eqsn  7056  fimax2g  7071  domunfican  7097  pwfi  7119  fissuni  7128  fipreima  7129  wofib  7228  wemapso  7234  sucprcreg  7281  noinfep  7328  noinfepOLD  7329  cantnfval2  7338  cantnfp1lem3  7350  tcidm  7399  tc0  7400  r1rankidb  7444  r1pw  7485  rankr1id  7502  scott0  7524  htalem  7534  xpomen  7611  infpwfien  7657  alephsmo  7697  dfac12lem3  7739  ackbij2lem4  7836  cflem  7840  cflecard  7847  cflim2  7857  cfslb  7860  fin4en1  7903  fin23lem13  7926  fin23lem15  7928  fin23lem36  7942  isf32lem1  7947  fin67  7989  dcomex  8041  zorn2lem4  8094  alephexp2  8171  fpwwe2lem13  8232  canthnumlem  8238  wunex2  8328  wuncidm  8336  eltsk2g  8341  axgroth6  8418  axgroth3  8421  xrsup  10938  expcl  11087  hashcard  11315  hashf1lem2  11359  lo1eq  12007  rlimeq  12008  serclim0  12016  isercolllem2  12104  isercoll  12106  summolem3  12152  isum  12157  fsumser  12168  fsumcl  12171  fsum2d  12199  fsumabs  12224  fsumrlim  12234  fsumo1  12235  fsumiun  12244  flo1  12275  eflt  12359  xpnnenOLD  12450  rpnnen2lem3  12457  rpnnen2lem5  12459  rpnnen2lem11  12465  rpnnen2  12466  rexpen  12468  eulerthlem2  12812  ressid  13165  ressinbas  13166  mremre  13468  yon11  14000  yon12  14001  yon2  14002  yonpropd  14004  oppcyon  14005  yonffth  14020  p0le  14111  ple1  14112  oduclatb  14210  ipopos  14225  fpwipodrs  14229  submid  14390  mulgnncl  14544  mulgnn0cl  14545  mulgcl  14546  subgid  14585  cntrnsg  14779  sylow3lem5  14904  lsmss1  14937  lsmss2  14939  gsumzres  15156  gsumzcl  15157  gsumzf1o  15158  gsumadd  15167  gsumzsplit  15168  gsumzmhm  15172  gsumzoppg  15178  gsumzinv  15179  gsumsub  15181  gsum2d  15185  dprdfinv  15216  dprdf1  15230  dmdprdsplitlem  15234  dprd2db  15240  dpjidcl  15255  ablfac1eulem  15269  ablfac1eu  15270  ablfaclem2  15283  gsumdixp  15354  subrgid  15509  lss1  15658  lbsextlem1  15873  rlmbas  15910  rlmplusg  15911  rlm0  15912  rlmmulr  15913  rlmsca  15914  rlmsca2  15915  rlmvsca  15916  rlmtopn  15917  rlmds  15918  psrass1lem  16085  mplsubglem  16141  mpllsslem  16142  mplsubrglem  16145  mplcoe1  16171  mplbas2  16174  evlslem4  16207  psrbagev1  16209  evlslem2  16211  znf1o  16467  zntoslem  16472  css0  16551  topopn  16614  fiinbas  16652  topbas  16672  topcld  16734  clstop  16768  ntrtop  16769  opnneissb  16813  opnssneib  16814  opnneiid  16825  maxlp  16840  isperf2  16845  restopn2  16870  restperf  16876  idcn  16949  cnconst2  16973  lmres  16990  rncmp  17085  fiuncmp  17093  cmpfi  17097  concn  17114  1stcelcls  17149  llyidm  17176  nllyidm  17177  toplly  17178  kgentopon  17195  kgencn2  17214  ptpjpre1  17228  ptbasfi  17238  ptcld  17269  xkopt  17311  elqtop2  17354  qtopuni  17355  ptcmpfi  17466  fbssfi  17494  opnfbas  17499  filtop  17512  isfil2  17513  isfild  17515  fsubbas  17524  ssfg  17529  filssufilg  17568  ufileu  17576  imaelfm  17608  rnelfm  17610  fmfnfmlem4  17614  neiflim  17631  supnfcls  17677  fclscf  17682  flimfnfcls  17685  tsmsfbas  17772  xpsxmet  17906  xpsdsval  17907  xpsmet  17908  tmsxms  17994  tmsms  17995  imasf1oxms  17997  imasf1oms  17998  prdsxms  18038  prdsms  18039  tmsxpsval  18046  retopbas  18231  cnngp  18251  cnperf  18287  retopcon  18296  fsumcn  18336  abscncf  18367  recncf  18368  imcncf  18369  cjcncf  18370  mulc1cncf  18371  cncfcn1  18376  cncfmpt2f  18380  cncfmpt2ss  18381  cdivcncf  18382  negcncf  18383  negfcncf  18384  abscncfALT  18385  cnmpt2pc  18388  xrhmeo  18406  oprpiece1res1  18411  oprpiece1res2  18412  cnrehmeo  18413  iscau3  18666  caubl  18695  caublcls  18696  evthicc2  18782  ovolre  18846  volsuplem  18874  uniiccdif  18895  uniioovol  18896  uniiccvol  18897  uniioombllem3  18902  uniioombllem4  18903  uniioombllem5  18904  dyadmbllem  18916  volcn  18923  volivth  18924  itgfsum  19143  iblabslem  19144  iblabs  19145  bddmulibl  19155  cnlimc  19200  cnlimci  19201  dvres3  19225  dvres3a  19226  dvidlem  19227  dvcnp2  19231  dvcn  19232  dvnadd  19240  dvnres  19242  cpnord  19246  cpnres  19248  dvaddbr  19249  dvmulbr  19250  dvcmul  19255  dvcmulf  19256  dvcobr  19257  dvcjbr  19260  dvrec  19266  dvmptntr  19282  dvmptfsum  19284  dveflem  19288  dvef  19289  rolle  19299  dvlipcn  19303  c1liplem1  19305  dvgt0lem2  19312  dvivth  19319  lhop1lem  19322  dvfsumabs  19332  ftc1a  19346  ftc1cn  19352  ftc2  19353  deg1mul3le  19464  plyssc  19544  plyeq0  19555  coeeulem  19568  0dgr  19589  coemulc  19598  coe0  19599  coesub  19600  coe1termlem  19601  dgrmulc  19614  dgrsub  19615  dgrcolem1  19616  dgrcolem2  19617  dvnply2  19629  plycpn  19631  plyremlem  19646  fta1lem  19649  vieta1lem2  19653  aalioulem3  19676  dvntaylp  19712  taylthlem1  19714  taylthlem2  19715  ulmcn  19738  psercn  19764  pserdv  19767  abelth  19779  efcn  19781  efcvx  19787  pige3  19847  dvrelog  19946  logcn  19956  dvloglem  19957  dvlog  19960  dvlog2  19962  efopnlem2  19966  logccv  19972  cxpcn  20047  cxpcn2  20048  cxpcn3  20050  resqrcn  20051  sqrcn  20052  loglesqr  20060  atancn  20194  rlimcnp3  20224  jensen  20245  ftalem3  20274  basellem2  20281  dchrfi  20456  dchrisumlema  20599  pntrsumo1  20676  pntrsumbnd  20677  pntlem3  20720  efghgrp  21000  sspid  21261  ssps  21266  helch  21783  hhssnv  21801  hhsssh  21806  shintcl  21869  chintcl  21871  shlesb1i  21925  omlsi  21943  chlejb1i  22015  chm0i  22029  chabs1  22055  chabs2  22056  spanun  22084  cmidi  22149  pjidmcoi  22717  csmdsymi  22874  sumdmdlem2  22959  dmdbr5ati  22962  mdcompli  22969  dmdcompli  22970  fdmrn  22996  cvmlift2lem6  23211  relexpdm  23404  relexprn  23405  rtrclreclem.refl  23413  rtrclreclem.subset  23414  trpredtr  23602  trpredpo  23607  frrlem5c  23656  frrlem10  23661  ontgval  24245  residcp  24443  prl2  24536  inpc  24644  inposet  24645  dominc  24647  rninc  24648  domncnt  24649  ranncnt  24650  dfps2  24656  toplat  24657  fsumprd  24696  clfsebs  24714  fincmpzer  24717  fprodadd  24719  fprodneg  24745  fprodsub  24746  caytr  24767  osneisi  24898  0alg  25123  catsbc  25216  tareltsuc  25265  prismorcsetlem  25279  prismorcset  25281  segline  25508  bsstrs  25513  segray  25522  rayline  25523  ivthALT  25625  fness  25649  ssref  25650  fneref  25651  refref  25652  refssfne  25661  fnemeet1  25682  fnejoin2  25685  filnetlem2  25695  filnetlem4  25697  welb  25784  caures  25843  constcncf  25845  addccncf  25846  idcncf  25847  sub1cncf  25848  sub2cncf  25849  cnresima  25851  rngoidl  26016  ralxpmap  26128  lcomfsup  26135  ismrcd1  26140  ismrc  26143  incssnn0  26153  mzpclall  26172  rmydioph  26474  rmxdioph  26476  expdiophlem2  26482  expdioph  26483  aomclem6  26523  kelac1  26528  frlmsslsp  26615  frlmlbs  26616  frlmup1  26617  gicabl  26630  rgspnid  26744  symggen  26778  lhe4.4ex1a  26913  dvsconst  26914  dvsid  26915  dvsef  26916  dvconstbi  26918  onfrALTlem3  27362  onfrALTlem3VD  27713  bnj1253  28096  atpsubN  29109  pol1N  29266  1psubclN  29300  cdlemefrs32fva  29756  dia2dimlem13  30433  dibord  30516  dochvalr  30714  hdmapevec  31195
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator