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

Theorem ssid 3369
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 21 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3354 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  eqimssi  3404  eqimss2i  3405  nsspssun  3576  inv1  3656  disjpss  3680  difid  3698  pwidg  3813  elssuni  4045  unimax  4051  intmin  4072  rintn0  4184  ordunidif  4632  iunpw  4762  onsucuni  4811  tfisi  4841  xpss1  4987  xpss2  4988  residm  5180  resdm  5187  resmpt3  5195  ssrnres  5312  dffn3  5601  fimacnv  5865  fparlem3  6451  fparlem4  6452  tfrlem1  6639  tz7.48-2  6702  abianfp  6719  oaordi  6792  omwordi  6817  omass  6826  nnaordi  6864  nnmwordi  6881  fpmg  7042  boxcutc  7108  domss2  7269  0fin  7339  en1eqsn  7341  fimax2g  7356  domunfican  7382  pwfi  7405  fissuni  7414  fipreima  7415  wofib  7517  wemapso  7523  sucprcreg  7570  noinfep  7617  noinfepOLD  7618  cantnfval2  7627  cantnfp1lem3  7639  tcidm  7688  tc0  7689  r1rankidb  7733  r1pw  7774  rankr1id  7791  scott0  7815  htalem  7825  xpomen  7902  infpwfien  7948  alephsmo  7988  dfac12lem3  8030  ackbij2lem4  8127  cflem  8131  cflecard  8138  cflim2  8148  cfslb  8151  fin4en1  8194  fin23lem13  8217  fin23lem15  8219  fin23lem36  8233  isf32lem1  8238  fin67  8280  dcomex  8332  zorn2lem4  8384  alephexp2  8461  fpwwe2lem13  8522  canthnumlem  8528  wunex2  8618  wuncidm  8626  eltsk2g  8631  axgroth6  8708  axgroth3  8711  xrsup  11254  expcl  11404  hashcard  11643  hashf1lem2  11710  lo1eq  12367  rlimeq  12368  serclim0  12376  isercolllem2  12464  isercoll  12466  summolem3  12513  isum  12518  fsumser  12529  fsumcl  12532  fsum2d  12560  fsumabs  12585  fsumrlim  12595  fsumo1  12596  fsumiun  12605  flo1  12639  eflt  12723  xpnnenOLD  12814  rpnnen2lem3  12821  rpnnen2lem5  12823  rpnnen2lem11  12829  rpnnen2  12830  rexpen  12832  eulerthlem2  13176  ressid  13529  ressinbas  13530  mremre  13834  yon11  14366  yon12  14367  yon2  14368  yonpropd  14370  oppcyon  14371  yonffth  14386  p0le  14477  ple1  14478  oduclatb  14576  ipopos  14591  fpwipodrs  14595  submid  14756  mulgnncl  14910  mulgnn0cl  14911  mulgcl  14912  subgid  14951  cntrnsg  15145  sylow3lem5  15270  lsmss1  15303  lsmss2  15305  gsumzres  15522  gsumzcl  15523  gsumzf1o  15524  gsumadd  15533  gsumzsplit  15534  gsumzmhm  15538  gsumzoppg  15544  gsumzinv  15545  gsumsub  15547  gsum2d  15551  dprdfinv  15582  dprdf1  15596  dmdprdsplitlem  15600  dprd2db  15606  dpjidcl  15621  ablfac1eulem  15635  ablfac1eu  15636  ablfaclem2  15649  gsumdixp  15720  subrgid  15875  lss1  16020  lbsextlem1  16235  rlmbas  16272  rlmplusg  16273  rlm0  16274  rlmmulr  16275  rlmsca  16276  rlmsca2  16277  rlmvsca  16278  rlmtopn  16279  rlmds  16280  psrass1lem  16447  mplsubglem  16503  mpllsslem  16504  mplsubrglem  16507  mplcoe1  16533  mplbas2  16536  evlslem4  16569  psrbagev1  16571  evlslem2  16573  znf1o  16837  zntoslem  16842  css0  16921  topopn  16984  fiinbas  17022  topbas  17042  topcld  17104  clstop  17138  ntrtop  17139  opnneissb  17183  opnssneib  17184  opnneiid  17195  neiptopuni  17199  neiptoptop  17200  maxlp  17216  isperf2  17221  restopn2  17246  restperf  17253  idcn  17326  cnconst2  17352  lmres  17369  rncmp  17464  fiuncmp  17472  cmpfi  17476  concn  17494  1stcelcls  17529  llyidm  17556  nllyidm  17557  toplly  17558  kgentopon  17575  kgencn2  17594  ptpjpre1  17608  ptbasfi  17618  ptcld  17650  xkopt  17692  elqtop2  17738  qtopuni  17739  ptcmpfi  17850  fbssfi  17874  opnfbas  17879  filtop  17892  isfil2  17893  isfild  17895  fsubbas  17904  ssfg  17909  filssufilg  17948  ufileu  17956  imaelfm  17988  rnelfm  17990  fmfnfmlem4  17994  neiflim  18011  supnfcls  18057  fclscf  18062  flimfnfcls  18065  tsmsfbas  18162  utopbas  18270  xpsxmet  18415  xpsdsval  18416  xpsmet  18417  tmsxms  18521  tmsms  18522  imasf1oxms  18524  imasf1oms  18525  prdsxms  18565  prdsms  18566  tmsxpsval  18573  retopbas  18799  cnngp  18819  cnperf  18856  retopcon  18865  fsumcn  18905  abscncf  18936  recncf  18937  imcncf  18938  cjcncf  18939  mulc1cncf  18940  cncfcn1  18945  cncfmpt2f  18949  cncfmpt2ss  18950  addccncf  18951  cdivcncf  18952  negcncf  18953  negfcncf  18954  abscncfALT  18955  cnmpt2pc  18958  xrhmeo  18976  oprpiece1res1  18981  oprpiece1res2  18982  cnrehmeo  18983  iscau3  19236  caubl  19265  caublcls  19266  evthicc2  19362  ovolre  19426  volsuplem  19454  uniiccdif  19475  uniioovol  19476  uniiccvol  19477  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  dyadmbllem  19496  volcn  19503  volivth  19504  itgfsum  19721  iblabslem  19722  iblabs  19723  bddmulibl  19733  cnlimc  19780  cnlimci  19781  dvres3  19805  dvres3a  19806  dvidlem  19807  dvcnp2  19811  dvcn  19812  dvnadd  19820  dvnres  19822  cpnord  19826  cpnres  19828  dvaddbr  19829  dvmulbr  19830  dvcmul  19835  dvcmulf  19836  dvcobr  19837  dvcjbr  19840  dvrec  19846  dvmptntr  19862  dvmptfsum  19864  dveflem  19868  dvef  19869  rolle  19879  dvlipcn  19883  c1liplem1  19885  dvgt0lem2  19892  dvivth  19899  lhop1lem  19902  dvfsumabs  19912  ftc1a  19926  ftc1cn  19932  ftc2  19933  deg1mul3le  20044  plyssc  20124  plyeq0  20135  coeeulem  20148  0dgr  20169  coemulc  20178  coe0  20179  coesub  20180  coe1termlem  20181  dgrmulc  20194  dgrsub  20195  dgrcolem1  20196  dgrcolem2  20197  dvnply2  20209  plycpn  20211  plyremlem  20226  fta1lem  20229  vieta1lem2  20233  aalioulem3  20256  dvntaylp  20292  taylthlem1  20294  taylthlem2  20295  ulmcn  20320  psercn  20347  pserdv  20350  abelth  20362  efcn  20364  efcvx  20370  pige3  20430  dvrelog  20533  logcn  20543  dvloglem  20544  dvlog  20547  dvlog2  20549  efopnlem2  20553  logccv  20559  cxpcn  20634  cxpcn2  20635  cxpcn3  20637  resqrcn  20638  sqrcn  20639  loglesqr  20647  atancn  20781  rlimcnp3  20811  jensen  20832  ftalem3  20862  basellem2  20869  dchrfi  21044  dchrisumlema  21187  pntrsumo1  21264  pntrsumbnd  21265  pntlem3  21308  cusgrasizeindslem2  21488  efghgrp  21966  sspid  22229  ssps  22234  helch  22751  hhssnv  22769  hhsssh  22774  shintcl  22837  chintcl  22839  shlesb1i  22893  omlsi  22911  chlejb1i  22983  chm0i  22997  chabs1  23023  chabs2  23024  spanun  23052  cmidi  23117  pjidmcoi  23685  csmdsymi  23842  sumdmdlem2  23927  dmdbr5ati  23930  mdcompli  23937  dmdcompli  23938  disjdifprg  24022  fdmrn  24044  xppreima  24064  xrinfm  24126  clatp0ex  24198  clatp1ex  24199  xrsmulgzz  24205  xrsp0  24208  xrsp1  24209  pnfneige0  24341  esumsn  24461  esumcvg  24481  pwsiga  24518  sigagenid  24539  lgamgulmlem2  24819  cvmlift2lem6  25000  relexpdm  25140  relexprn  25141  rtrclreclem.refl  25149  rtrclreclem.subset  25150  prodmolem3  25264  iprod  25269  iprodn0  25271  fprodss  25279  fprodcl  25283  fprod2d  25310  risefaccl  25336  fallfaccl  25337  trpredtr  25513  trpredpo  25518  wzel  25580  frrlem5c  25593  frrlem10  25598  imagesset  25803  ontgval  26186  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  mbfposadd  26266  ftc1cnnclem  26292  ftc1cnnc  26293  ftc1anc  26302  ftc2nc  26303  areacirclem2  26307  areacirclem3  26308  areacirclem4  26309  areacirc  26311  ivthALT  26352  fness  26376  ssref  26377  fneref  26378  refref  26379  refssfne  26388  fnemeet1  26409  fnejoin2  26412  filnetlem2  26422  filnetlem4  26424  welb  26452  caures  26480  constcncf  26482  idcncf  26483  sub1cncf  26484  sub2cncf  26485  cnresima  26487  rngoidl  26648  ralxpmap  26756  lcomfsup  26761  ismrcd1  26766  ismrc  26769  incssnn0  26779  mzpclall  26798  rmydioph  27099  rmxdioph  27101  expdiophlem2  27107  expdioph  27108  aomclem6  27148  kelac1  27152  frlmsslsp  27239  frlmlbs  27240  frlmup1  27241  gicabl  27254  rgspnid  27368  symggen  27402  lhe4.4ex1a  27537  dvsconst  27538  dvsid  27539  dvsef  27540  dvconstbi  27542  dvcosre  27731  itgsinexplem1  27738  funresfunco  27979  onfrALTlem3  28704  onfrALTlem3VD  29073  bnj1253  29460  atpsubN  30624  pol1N  30781  1psubclN  30815  cdlemefrs32fva  31271  dia2dimlem13  31948  dibord  32031  dochvalr  32229  hdmapevec  32710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator