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

Theorem ssid 3199
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
Dummy variable  x is distinct from all other variables.

Proof of Theorem ssid
StepHypRef Expression
1 id 21 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3186 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1685    C_ wss 3154
This theorem is referenced by:  eqimssi  3234  eqimss2i  3235  nsspssun  3404  inv1  3483  disjpss  3507  difid  3524  pwidg  3639  elssuni  3857  unimax  3863  intmin  3884  rintn0  3994  ordunidif  4440  iunpw  4570  onsucuni  4619  tfisi  4649  xpss1  4795  xpss2  4796  residm  4986  resdm  4993  resmpt3  5001  ssrnres  5116  dffn3  5362  fimacnv  5619  fparlem3  6182  fparlem4  6183  tfrlem1  6387  tz7.48-2  6450  abianfp  6467  oaordi  6540  omwordi  6565  omass  6574  nnaordi  6612  nnmwordi  6629  fpmg  6789  boxcutc  6855  domss2  7016  0fin  7083  en1eqsn  7084  fimax2g  7099  domunfican  7125  pwfi  7147  fissuni  7156  fipreima  7157  wofib  7256  wemapso  7262  sucprcreg  7309  noinfep  7356  noinfepOLD  7357  cantnfval2  7366  cantnfp1lem3  7378  tcidm  7427  tc0  7428  r1rankidb  7472  r1pw  7513  rankr1id  7530  scott0  7552  htalem  7562  xpomen  7639  infpwfien  7685  alephsmo  7725  dfac12lem3  7767  ackbij2lem4  7864  cflem  7868  cflecard  7875  cflim2  7885  cfslb  7888  fin4en1  7931  fin23lem13  7954  fin23lem15  7956  fin23lem36  7970  isf32lem1  7975  fin67  8017  dcomex  8069  zorn2lem4  8122  alephexp2  8199  fpwwe2lem13  8260  canthnumlem  8266  wunex2  8356  wuncidm  8364  eltsk2g  8369  axgroth6  8446  axgroth3  8449  xrsup  10967  expcl  11116  hashcard  11344  hashf1lem2  11389  lo1eq  12037  rlimeq  12038  serclim0  12046  isercolllem2  12134  isercoll  12136  summolem3  12182  isum  12187  fsumser  12198  fsumcl  12201  fsum2d  12229  fsumabs  12254  fsumrlim  12264  fsumo1  12265  fsumiun  12274  flo1  12308  eflt  12392  xpnnenOLD  12483  rpnnen2lem3  12490  rpnnen2lem5  12492  rpnnen2lem11  12498  rpnnen2  12499  rexpen  12501  eulerthlem2  12845  ressid  13198  ressinbas  13199  mremre  13501  yon11  14033  yon12  14034  yon2  14035  yonpropd  14037  oppcyon  14038  yonffth  14053  p0le  14144  ple1  14145  oduclatb  14243  ipopos  14258  fpwipodrs  14262  submid  14423  mulgnncl  14577  mulgnn0cl  14578  mulgcl  14579  subgid  14618  cntrnsg  14812  sylow3lem5  14937  lsmss1  14970  lsmss2  14972  gsumzres  15189  gsumzcl  15190  gsumzf1o  15191  gsumadd  15200  gsumzsplit  15201  gsumzmhm  15205  gsumzoppg  15211  gsumzinv  15212  gsumsub  15214  gsum2d  15218  dprdfinv  15249  dprdf1  15263  dmdprdsplitlem  15267  dprd2db  15273  dpjidcl  15288  ablfac1eulem  15302  ablfac1eu  15303  ablfaclem2  15316  gsumdixp  15387  subrgid  15542  lss1  15691  lbsextlem1  15906  rlmbas  15943  rlmplusg  15944  rlm0  15945  rlmmulr  15946  rlmsca  15947  rlmsca2  15948  rlmvsca  15949  rlmtopn  15950  rlmds  15951  psrass1lem  16118  mplsubglem  16174  mpllsslem  16175  mplsubrglem  16178  mplcoe1  16204  mplbas2  16207  evlslem4  16240  psrbagev1  16242  evlslem2  16244  znf1o  16500  zntoslem  16505  css0  16584  topopn  16647  fiinbas  16685  topbas  16705  topcld  16767  clstop  16801  ntrtop  16802  opnneissb  16846  opnssneib  16847  opnneiid  16858  maxlp  16873  isperf2  16878  restopn2  16903  restperf  16909  idcn  16982  cnconst2  17006  lmres  17023  rncmp  17118  fiuncmp  17126  cmpfi  17130  concn  17147  1stcelcls  17182  llyidm  17209  nllyidm  17210  toplly  17211  kgentopon  17228  kgencn2  17247  ptpjpre1  17261  ptbasfi  17271  ptcld  17302  xkopt  17344  elqtop2  17387  qtopuni  17388  ptcmpfi  17499  fbssfi  17527  opnfbas  17532  filtop  17545  isfil2  17546  isfild  17548  fsubbas  17557  ssfg  17562  filssufilg  17601  ufileu  17609  imaelfm  17641  rnelfm  17643  fmfnfmlem4  17647  neiflim  17664  supnfcls  17710  fclscf  17715  flimfnfcls  17718  tsmsfbas  17805  xpsxmet  17939  xpsdsval  17940  xpsmet  17941  tmsxms  18027  tmsms  18028  imasf1oxms  18030  imasf1oms  18031  prdsxms  18071  prdsms  18072  tmsxpsval  18079  retopbas  18264  cnngp  18284  cnperf  18320  retopcon  18329  fsumcn  18369  abscncf  18400  recncf  18401  imcncf  18402  cjcncf  18403  mulc1cncf  18404  cncfcn1  18409  cncfmpt2f  18413  cncfmpt2ss  18414  cdivcncf  18415  negcncf  18416  negfcncf  18417  abscncfALT  18418  cnmpt2pc  18421  xrhmeo  18439  oprpiece1res1  18444  oprpiece1res2  18445  cnrehmeo  18446  iscau3  18699  caubl  18728  caublcls  18729  evthicc2  18815  ovolre  18879  volsuplem  18907  uniiccdif  18928  uniioovol  18929  uniiccvol  18930  uniioombllem3  18935  uniioombllem4  18936  uniioombllem5  18937  dyadmbllem  18949  volcn  18956  volivth  18957  itgfsum  19176  iblabslem  19177  iblabs  19178  bddmulibl  19188  cnlimc  19233  cnlimci  19234  dvres3  19258  dvres3a  19259  dvidlem  19260  dvcnp2  19264  dvcn  19265  dvnadd  19273  dvnres  19275  cpnord  19279  cpnres  19281  dvaddbr  19282  dvmulbr  19283  dvcmul  19288  dvcmulf  19289  dvcobr  19290  dvcjbr  19293  dvrec  19299  dvmptntr  19315  dvmptfsum  19317  dveflem  19321  dvef  19322  rolle  19332  dvlipcn  19336  c1liplem1  19338  dvgt0lem2  19345  dvivth  19352  lhop1lem  19355  dvfsumabs  19365  ftc1a  19379  ftc1cn  19385  ftc2  19386  deg1mul3le  19497  plyssc  19577  plyeq0  19588  coeeulem  19601  0dgr  19622  coemulc  19631  coe0  19632  coesub  19633  coe1termlem  19634  dgrmulc  19647  dgrsub  19648  dgrcolem1  19649  dgrcolem2  19650  dvnply2  19662  plycpn  19664  plyremlem  19679  fta1lem  19682  vieta1lem2  19686  aalioulem3  19709  dvntaylp  19745  taylthlem1  19747  taylthlem2  19748  ulmcn  19771  psercn  19797  pserdv  19800  abelth  19812  efcn  19814  efcvx  19820  pige3  19880  dvrelog  19979  logcn  19989  dvloglem  19990  dvlog  19993  dvlog2  19995  efopnlem2  19999  logccv  20005  cxpcn  20080  cxpcn2  20081  cxpcn3  20083  resqrcn  20084  sqrcn  20085  loglesqr  20093  atancn  20227  rlimcnp3  20257  jensen  20278  ftalem3  20307  basellem2  20314  dchrfi  20489  dchrisumlema  20632  pntrsumo1  20709  pntrsumbnd  20710  pntlem3  20753  efghgrp  21033  sspid  21294  ssps  21299  helch  21816  hhssnv  21834  hhsssh  21839  shintcl  21902  chintcl  21904  shlesb1i  21958  omlsi  21976  chlejb1i  22048  chm0i  22062  chabs1  22088  chabs2  22089  spanun  22117  cmidi  22182  pjidmcoi  22750  csmdsymi  22907  sumdmdlem2  22992  dmdbr5ati  22995  mdcompli  23002  dmdcompli  23003  fdmrn  23029  cvmlift2lem6  23244  relexpdm  23437  relexprn  23438  rtrclreclem.refl  23446  rtrclreclem.subset  23447  trpredtr  23635  trpredpo  23640  frrlem5c  23689  frrlem10  23694  ontgval  24278  residcp  24476  prl2  24569  inpc  24677  inposet  24678  dominc  24680  rninc  24681  domncnt  24682  ranncnt  24683  dfps2  24689  toplat  24690  fsumprd  24729  clfsebs  24747  fincmpzer  24750  fprodadd  24752  fprodneg  24778  fprodsub  24779  caytr  24800  osneisi  24931  0alg  25156  catsbc  25249  tareltsuc  25298  prismorcsetlem  25312  prismorcset  25314  segline  25541  bsstrs  25546  segray  25555  rayline  25556  ivthALT  25658  fness  25682  ssref  25683  fneref  25684  refref  25685  refssfne  25694  fnemeet1  25715  fnejoin2  25718  filnetlem2  25728  filnetlem4  25730  welb  25817  caures  25876  constcncf  25878  addccncf  25879  idcncf  25880  sub1cncf  25881  sub2cncf  25882  cnresima  25884  rngoidl  26049  ralxpmap  26161  lcomfsup  26168  ismrcd1  26173  ismrc  26176  incssnn0  26186  mzpclall  26205  rmydioph  26507  rmxdioph  26509  expdiophlem2  26515  expdioph  26516  aomclem6  26556  kelac1  26561  frlmsslsp  26648  frlmlbs  26649  frlmup1  26650  gicabl  26663  rgspnid  26777  symggen  26811  lhe4.4ex1a  26946  dvsconst  26947  dvsid  26948  dvsef  26949  dvconstbi  26951  dvcosre  27141  itgsinexplem1  27148  funresfunco  27368  onfrALTlem3  27581  onfrALTlem3VD  27932  bnj1253  28315  atpsubN  29210  pol1N  29367  1psubclN  29401  cdlemefrs32fva  29857  dia2dimlem13  30534  dibord  30617  dochvalr  30815  hdmapevec  31296
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator