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

Theorem ssid 3359
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 3344 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  eqimssi  3394  eqimss2i  3395  nsspssun  3566  inv1  3646  disjpss  3670  difid  3688  pwidg  3803  elssuni  4035  unimax  4041  intmin  4062  rintn0  4173  ordunidif  4621  iunpw  4751  onsucuni  4800  tfisi  4830  xpss1  4976  xpss2  4977  residm  5169  resdm  5176  resmpt3  5184  ssrnres  5301  dffn3  5590  fimacnv  5854  fparlem3  6440  fparlem4  6441  tfrlem1  6628  tz7.48-2  6691  abianfp  6708  oaordi  6781  omwordi  6806  omass  6815  nnaordi  6853  nnmwordi  6870  fpmg  7031  boxcutc  7097  domss2  7258  0fin  7328  en1eqsn  7330  fimax2g  7345  domunfican  7371  pwfi  7394  fissuni  7403  fipreima  7404  wofib  7506  wemapso  7512  sucprcreg  7559  noinfep  7606  noinfepOLD  7607  cantnfval2  7616  cantnfp1lem3  7628  tcidm  7677  tc0  7678  r1rankidb  7722  r1pw  7763  rankr1id  7780  scott0  7802  htalem  7812  xpomen  7889  infpwfien  7935  alephsmo  7975  dfac12lem3  8017  ackbij2lem4  8114  cflem  8118  cflecard  8125  cflim2  8135  cfslb  8138  fin4en1  8181  fin23lem13  8204  fin23lem15  8206  fin23lem36  8220  isf32lem1  8225  fin67  8267  dcomex  8319  zorn2lem4  8371  alephexp2  8448  fpwwe2lem13  8509  canthnumlem  8515  wunex2  8605  wuncidm  8613  eltsk2g  8618  axgroth6  8695  axgroth3  8698  xrsup  11241  expcl  11391  hashcard  11630  hashf1lem2  11697  lo1eq  12354  rlimeq  12355  serclim0  12363  isercolllem2  12451  isercoll  12453  summolem3  12500  isum  12505  fsumser  12516  fsumcl  12519  fsum2d  12547  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  flo1  12626  eflt  12710  xpnnenOLD  12801  rpnnen2lem3  12808  rpnnen2lem5  12810  rpnnen2lem11  12816  rpnnen2  12817  rexpen  12819  eulerthlem2  13163  ressid  13516  ressinbas  13517  mremre  13821  yon11  14353  yon12  14354  yon2  14355  yonpropd  14357  oppcyon  14358  yonffth  14373  p0le  14464  ple1  14465  oduclatb  14563  ipopos  14578  fpwipodrs  14582  submid  14743  mulgnncl  14897  mulgnn0cl  14898  mulgcl  14899  subgid  14938  cntrnsg  15132  sylow3lem5  15257  lsmss1  15290  lsmss2  15292  gsumzres  15509  gsumzcl  15510  gsumzf1o  15511  gsumadd  15520  gsumzsplit  15521  gsumzmhm  15525  gsumzoppg  15531  gsumzinv  15532  gsumsub  15534  gsum2d  15538  dprdfinv  15569  dprdf1  15583  dmdprdsplitlem  15587  dprd2db  15593  dpjidcl  15608  ablfac1eulem  15622  ablfac1eu  15623  ablfaclem2  15636  gsumdixp  15707  subrgid  15862  lss1  16007  lbsextlem1  16222  rlmbas  16259  rlmplusg  16260  rlm0  16261  rlmmulr  16262  rlmsca  16263  rlmsca2  16264  rlmvsca  16265  rlmtopn  16266  rlmds  16267  psrass1lem  16434  mplsubglem  16490  mpllsslem  16491  mplsubrglem  16494  mplcoe1  16520  mplbas2  16523  evlslem4  16556  psrbagev1  16558  evlslem2  16560  znf1o  16824  zntoslem  16829  css0  16908  topopn  16971  fiinbas  17009  topbas  17029  topcld  17091  clstop  17125  ntrtop  17126  opnneissb  17170  opnssneib  17171  opnneiid  17182  neiptopuni  17186  neiptoptop  17187  maxlp  17203  isperf2  17208  restopn2  17233  restperf  17240  idcn  17313  cnconst2  17339  lmres  17356  rncmp  17451  fiuncmp  17459  cmpfi  17463  concn  17481  1stcelcls  17516  llyidm  17543  nllyidm  17544  toplly  17545  kgentopon  17562  kgencn2  17581  ptpjpre1  17595  ptbasfi  17605  ptcld  17637  xkopt  17679  elqtop2  17725  qtopuni  17726  ptcmpfi  17837  fbssfi  17861  opnfbas  17866  filtop  17879  isfil2  17880  isfild  17882  fsubbas  17891  ssfg  17896  filssufilg  17935  ufileu  17943  imaelfm  17975  rnelfm  17977  fmfnfmlem4  17981  neiflim  17998  supnfcls  18044  fclscf  18049  flimfnfcls  18052  tsmsfbas  18149  utopbas  18257  xpsxmet  18402  xpsdsval  18403  xpsmet  18404  tmsxms  18508  tmsms  18509  imasf1oxms  18511  imasf1oms  18512  prdsxms  18552  prdsms  18553  tmsxpsval  18560  retopbas  18786  cnngp  18806  cnperf  18843  retopcon  18852  fsumcn  18892  abscncf  18923  recncf  18924  imcncf  18925  cjcncf  18926  mulc1cncf  18927  cncfcn1  18932  cncfmpt2f  18936  cncfmpt2ss  18937  addccncf  18938  cdivcncf  18939  negcncf  18940  negfcncf  18941  abscncfALT  18942  cnmpt2pc  18945  xrhmeo  18963  oprpiece1res1  18968  oprpiece1res2  18969  cnrehmeo  18970  iscau3  19223  caubl  19252  caublcls  19253  evthicc2  19349  ovolre  19413  volsuplem  19441  uniiccdif  19462  uniioovol  19463  uniiccvol  19464  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  dyadmbllem  19483  volcn  19490  volivth  19491  itgfsum  19710  iblabslem  19711  iblabs  19712  bddmulibl  19722  cnlimc  19767  cnlimci  19768  dvres3  19792  dvres3a  19793  dvidlem  19794  dvcnp2  19798  dvcn  19799  dvnadd  19807  dvnres  19809  cpnord  19813  cpnres  19815  dvaddbr  19816  dvmulbr  19817  dvcmul  19822  dvcmulf  19823  dvcobr  19824  dvcjbr  19827  dvrec  19833  dvmptntr  19849  dvmptfsum  19851  dveflem  19855  dvef  19856  rolle  19866  dvlipcn  19870  c1liplem1  19872  dvgt0lem2  19879  dvivth  19886  lhop1lem  19889  dvfsumabs  19899  ftc1a  19913  ftc1cn  19919  ftc2  19920  deg1mul3le  20031  plyssc  20111  plyeq0  20122  coeeulem  20135  0dgr  20156  coemulc  20165  coe0  20166  coesub  20167  coe1termlem  20168  dgrmulc  20181  dgrsub  20182  dgrcolem1  20183  dgrcolem2  20184  dvnply2  20196  plycpn  20198  plyremlem  20213  fta1lem  20216  vieta1lem2  20220  aalioulem3  20243  dvntaylp  20279  taylthlem1  20281  taylthlem2  20282  ulmcn  20307  psercn  20334  pserdv  20337  abelth  20349  efcn  20351  efcvx  20357  pige3  20417  dvrelog  20520  logcn  20530  dvloglem  20531  dvlog  20534  dvlog2  20536  efopnlem2  20540  logccv  20546  cxpcn  20621  cxpcn2  20622  cxpcn3  20624  resqrcn  20625  sqrcn  20626  loglesqr  20634  atancn  20768  rlimcnp3  20798  jensen  20819  ftalem3  20849  basellem2  20856  dchrfi  21031  dchrisumlema  21174  pntrsumo1  21251  pntrsumbnd  21252  pntlem3  21295  cusgrasizeindslem2  21475  efghgrp  21953  sspid  22216  ssps  22221  helch  22738  hhssnv  22756  hhsssh  22761  shintcl  22824  chintcl  22826  shlesb1i  22880  omlsi  22898  chlejb1i  22970  chm0i  22984  chabs1  23010  chabs2  23011  spanun  23039  cmidi  23104  pjidmcoi  23672  csmdsymi  23829  sumdmdlem2  23914  dmdbr5ati  23917  mdcompli  23924  dmdcompli  23925  disjdifprg  24009  fdmrn  24031  xppreima  24051  xrinfm  24113  clatp0ex  24185  clatp1ex  24186  xrsmulgzz  24192  xrsp0  24195  xrsp1  24196  pnfneige0  24328  esumsn  24448  esumcvg  24468  pwsiga  24505  sigagenid  24526  lgamgulmlem2  24806  cvmlift2lem6  24987  relexpdm  25127  relexprn  25128  rtrclreclem.refl  25136  rtrclreclem.subset  25137  prodmolem3  25251  iprod  25256  iprodn0  25258  fprodss  25266  fprodcl  25270  fprod2d  25297  risefaccl  25323  fallfaccl  25324  trpredtr  25500  trpredpo  25505  wzel  25567  frrlem5c  25580  frrlem10  25585  imagesset  25790  ontgval  26173  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  mbfposadd  26244  ftc1cnnclem  26268  ftc1cnnc  26269  ftc1anc  26278  ftc2nc  26279  areacirclem3  26283  areacirclem4  26284  areacirclem1  26285  areacirclem5  26286  ivthALT  26329  fness  26353  ssref  26354  fneref  26355  refref  26356  refssfne  26365  fnemeet1  26386  fnejoin2  26389  filnetlem2  26399  filnetlem4  26401  welb  26429  caures  26457  constcncf  26459  idcncf  26460  sub1cncf  26461  sub2cncf  26462  cnresima  26464  rngoidl  26625  ralxpmap  26733  lcomfsup  26738  ismrcd1  26743  ismrc  26746  incssnn0  26756  mzpclall  26775  rmydioph  27076  rmxdioph  27078  expdiophlem2  27084  expdioph  27085  aomclem6  27125  kelac1  27129  frlmsslsp  27216  frlmlbs  27217  frlmup1  27218  gicabl  27231  rgspnid  27345  symggen  27379  lhe4.4ex1a  27514  dvsconst  27515  dvsid  27516  dvsef  27517  dvconstbi  27519  dvcosre  27708  itgsinexplem1  27715  funresfunco  27956  onfrALTlem3  28567  onfrALTlem3VD  28936  bnj1253  29323  atpsubN  30487  pol1N  30644  1psubclN  30678  cdlemefrs32fva  31134  dia2dimlem13  31811  dibord  31894  dochvalr  32092  hdmapevec  32573
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator