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

Theorem ssid 3508
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 21-Jun-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 22 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 3493 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  eqimssi  3543  eqimss2i  3544  nsspssun  3728  inv1  3811  disjpss  3865  difid  3884  pwidg  4012  elssuni  4264  unimax  4270  intmin  4291  rintn0  4409  sseliALT  4570  ordunidif  4915  xpss1  5099  xpss2  5100  residm  5293  resdm  5303  resmpt3  5312  ssrnres  5430  dffn3  5720  fdmrn  5728  fvreseq1  5964  fimacnv  5995  iunpw  6587  onsucuni  6636  tfisi  6666  fparlem3  6875  fparlem4  6876  funsssuppss  6918  suppofss1d  6929  suppofss2d  6930  tfrlem1  7037  tz7.48-2  7099  oaordi  7187  omwordi  7212  omass  7221  nnaordi  7259  nnmwordi  7276  fpmg  7437  ralxpmap  7461  boxcutc  7505  domss2  7669  0fin  7740  en1eqsn  7742  findcard2d  7754  fimax2g  7758  domunfican  7785  pwfi  7807  fissuni  7817  fipreima  7818  fsuppmptif  7851  fsuppco2  7854  fsuppcor  7855  mapfienlem1  7856  mapfienlem2  7857  wofib  7962  wemapso  7968  noinfep  8067  noinfepOLD  8068  cantnfval2  8079  cantnfp1lem3  8090  cantnflem1  8099  cantnfval2OLD  8109  cantnfp1lem3OLD  8116  tcidm  8168  tc0  8169  r1rankidb  8213  r1pw  8254  rankr1id  8271  scott0  8295  htalem  8305  xpomen  8384  infpwfien  8434  alephsmo  8474  dfac12lem3  8516  ackbij2lem4  8613  cflem  8617  cflecard  8624  cflim2  8634  cfslb  8637  fin4en1  8680  fin23lem13  8703  fin23lem15  8705  fin23lem36  8719  isf32lem1  8724  fin67  8766  dcomex  8818  zorn2lem4  8870  alephexp2  8947  fpwwe2lem13  9009  canthnumlem  9015  wunex2  9105  wuncidm  9113  eltsk2g  9118  axgroth6  9195  axgroth3  9198  xrsup  11977  expcl  12166  hashcard  12409  hashf1lem2  12489  xptrrel  12898  cotrtrclfv  12930  rtrclreclem1  12973  rtrclreclem2  12974  lo1eq  13473  rlimeq  13474  serclim0  13482  isercolllem2  13570  isercoll  13572  summolem3  13618  isum  13623  fsumser  13634  fsumcl  13637  fsum2d  13668  fsumabs  13697  fsumrlim  13707  fsumo1  13708  fsumiun  13717  flo1  13748  prodmolem3  13822  iprod  13827  iprodn0  13829  fprodss  13837  fprodcl  13841  fprod2d  13867  eflt  13934  xpnnenOLD  14027  rpnnen2lem3  14034  rpnnen2lem5  14036  rpnnen2lem11  14042  rpnnen2  14043  rexpen  14045  eulerthlem2  14396  ressid  14778  ressinbas  14779  mremre  15093  catsubcat  15327  yon11  15732  yon12  15733  yon2  15734  yonpropd  15736  oppcyon  15737  yonffth  15752  oduclatb  15973  ipopos  15989  fpwipodrs  15993  submid  16181  mulgnncl  16356  mulgnn0cl  16357  mulgcl  16358  subgid  16402  cntrnsg  16578  symggen  16694  sylow3lem5  16850  lsmss1  16883  lsmss2  16885  gsumzres  17113  gsumzcl2  17114  gsumzf1o  17116  gsumzresOLD  17117  gsumzclOLD  17118  gsumzf1oOLD  17119  gsumadd  17137  gsumaddOLD  17138  gsumzsplitOLD  17144  gsumzmhm  17155  gsumzmhmOLD  17156  gsumzoppg  17165  gsumzoppgOLD  17166  gsumzinvOLD  17168  gsum2dlem1  17193  gsum2dlem2  17194  gsum2d  17195  gsum2dOLD  17196  dprdfinv  17254  dprdfinvOLD  17261  dprdf1  17275  dmdprdsplitlem  17279  dmdprdsplitlemOLD  17280  dprd2db  17287  dpjidcl  17302  dpjidclOLD  17309  ablfac1eulem  17318  ablfac1eu  17319  ablfaclem2  17332  gsumdixpOLD  17452  gsumdixp  17453  subrgid  17626  lcomfsupOLD  17744  lcomfsupp  17745  lss1  17780  lbsextlem1  17999  rlmval2  18035  rlmbas  18036  rlmplusg  18037  rlm0  18038  rlmmulr  18040  rlmsca  18041  rlmsca2  18042  rlmvsca  18043  rlmtopn  18044  rlmds  18045  psrass1lem  18224  mplsubglem  18288  mpllsslem  18289  mplsubglemOLD  18290  mpllsslemOLD  18291  mplsubrglem  18295  mplsubrglemOLD  18296  mplcoe1  18322  mplcoe5  18326  mplbas2  18329  mplbas2OLD  18330  evlslem4OLD  18368  evlslem4  18369  psrbagev1  18372  psrbagev1OLD  18373  evlslem2  18375  ply1coeOLD  18533  znf1o  18763  zntoslem  18768  regsumsupp  18831  css0  18893  uvcresum  18995  frlmsslsp  18998  frlmlbs  18999  frlmup1  19000  mamures  19059  mdetrsca2  19273  mdetrlin2  19276  mdetunilem5  19285  mdetunilem9  19289  smadiadetglem1  19340  smadiadetglem2  19341  pmatcollpw3  19452  cpmadumatpolylem2  19550  topopn  19582  fiinbas  19620  topbas  19641  topcld  19703  clstop  19737  ntrtop  19738  opnneissb  19782  opnssneib  19783  opnneiid  19794  neiptopuni  19798  neiptoptop  19799  maxlp  19815  isperf2  19820  restopn2  19845  restperf  19852  idcn  19925  cnconst2  19951  lmres  19968  rncmp  20063  fiuncmp  20071  cmpfi  20075  concn  20093  1stcelcls  20128  llyidm  20155  nllyidm  20156  toplly  20157  ssref  20179  refref  20180  kgentopon  20205  kgencn2  20224  ptpjpre1  20238  ptbasfi  20248  ptcld  20280  xkopt  20322  elqtop2  20368  qtopuni  20369  ptcmpfi  20480  fbssfi  20504  opnfbas  20509  filtop  20522  isfil2  20523  isfild  20525  fsubbas  20534  ssfg  20539  filssufilg  20578  ufileu  20586  imaelfm  20618  rnelfm  20620  fmfnfmlem4  20624  neiflim  20641  supnfcls  20687  fclscf  20692  flimfnfcls  20695  tsmsfbas  20792  utopbas  20904  xpsxmet  21049  xpsdsval  21050  xpsmet  21051  tmsxms  21155  tmsms  21156  imasf1oxms  21158  imasf1oms  21159  prdsxms  21199  prdsms  21200  tmsxpsval  21207  retopbas  21433  cnngp  21453  cnperf  21491  retopcon  21500  fsumcn  21540  abscncf  21571  recncf  21572  imcncf  21573  cjcncf  21574  mulc1cncf  21575  cncfcn1  21580  cncfmpt2f  21584  cncfmpt2ss  21585  addccncf  21586  cdivcncf  21587  negcncf  21588  negfcncf  21589  abscncfALT  21590  cnmpt2pc  21594  xrhmeo  21612  oprpiece1res1  21617  oprpiece1res2  21618  cnrehmeo  21619  iscau3  21883  caubl  21912  caublcls  21913  rrxcph  21990  rrxmval  21998  rrxdstprj1  22002  evthicc2  22038  ovolre  22102  volsuplem  22131  uniiccdif  22153  uniioovol  22154  uniiccvol  22155  uniioombllem3  22160  uniioombllem4  22161  uniioombllem5  22162  dyadmbllem  22174  volcn  22181  volivth  22182  itgfsum  22399  iblabslem  22400  iblabs  22401  bddmulibl  22411  cnlimc  22458  cnlimci  22459  dvres3  22483  dvres3a  22484  dvidlem  22485  dvcnp2  22489  dvcn  22490  dvnadd  22498  dvnres  22500  cpnord  22504  cpnres  22506  dvaddbr  22507  dvmulbr  22508  dvcmul  22513  dvcmulf  22514  dvcobr  22515  dvcjbr  22518  dvrec  22524  dvmptntr  22540  dvmptfsum  22542  dveflem  22546  dvef  22547  rolle  22557  dvlipcn  22561  c1liplem1  22563  dvgt0lem2  22570  dvivth  22577  lhop1lem  22580  dvfsumabs  22590  ftc1a  22604  ftc1cn  22610  ftc2  22611  deg1mul3le  22683  plyssc  22763  plyeq0  22774  coeeulem  22787  0dgr  22808  coemulc  22818  coe0  22819  coesub  22820  coe1termlem  22821  dgrmulc  22834  dgrsub  22835  dgrcolem1  22836  dgrcolem2  22837  dvnply2  22849  plycpn  22851  plyremlem  22866  fta1lem  22869  vieta1lem2  22873  aalioulem3  22896  dvntaylp  22932  taylthlem1  22934  taylthlem2  22935  ulmcn  22960  psercn  22987  pserdv  22990  abelth  23002  efcn  23004  efcvx  23010  pige3  23076  dvrelog  23186  logcn  23196  dvloglem  23197  dvlog  23200  dvlog2  23202  efopnlem2  23206  logccv  23212  cxpcn  23287  cxpcn2  23288  cxpcn3  23290  resqrtcn  23291  sqrtcn  23292  loglesqrt  23300  atancn  23464  rlimcnp3  23495  jensen  23516  ftalem3  23546  basellem2  23553  dchrfi  23728  dchrisumlema  23871  pntrsumo1  23948  pntrsumbnd  23949  pntlem3  23992  cusgrasizeindslem2  24676  efghgrpOLD  25573  sspid  25836  ssps  25841  helch  26359  hhssnv  26378  hhsssh  26383  shintcl  26446  chintcl  26448  shlesb1i  26502  omlsi  26520  chlejb1i  26592  chm0i  26606  chabs1  26632  chabs2  26633  spanun  26661  cmidi  26726  pjidmcoi  27294  csmdsymi  27451  sumdmdlem2  27536  dmdbr5ati  27539  mdcompli  27546  dmdcompli  27547  disjdifprg  27646  fcoinver  27674  xppreima  27708  padct  27776  xrinfm  27806  clatp0cl  27893  clatp1cl  27894  xrsmulgzz  27900  xrsp0  27903  xrsp1  27904  gsumle  28004  gsummpt2co  28005  gsumvsca1  28008  gsumvsca2  28009  reff  28077  locfinreflem  28078  pnfneige0  28168  esumsnf  28293  esumcvg  28315  pwsiga  28360  sigagenid  28381  baselcarsg  28514  lgamgulmlem2  28836  cvmlift2lem6  29017  mrsubrn  29137  mrsubff1  29138  mrsub0  29140  mrsubccat  29142  mrsubcn  29143  elmrsubrn  29144  elmsubrn  29152  msubrn  29153  msubff1  29180  mthmpps  29206  risefaccl  29378  fallfaccl  29379  trpredtr  29553  trpredpo  29558  wzel  29620  frrlem5c  29633  frrlem10  29638  imagesset  29831  ontgval  30124  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  mbfposadd  30302  ftc1cnnclem  30328  ftc1cnnc  30329  ftc1anc  30338  ftc2nc  30339  areacirclem2  30348  areacirclem3  30349  areacirclem4  30350  areacirc  30352  ivthALT  30393  fness  30407  fneref  30408  refssfne  30416  fnemeet1  30424  fnejoin2  30427  filnetlem2  30437  filnetlem4  30439  welb  30467  caures  30493  constcncf  30495  idcncf  30496  sub1cncf  30497  sub2cncf  30498  cnresima  30500  rngoidl  30661  ismrcd1  30870  ismrc  30873  incssnn0  30883  mzpclall  30899  rmydioph  31195  rmxdioph  31197  expdiophlem2  31203  expdioph  31204  aomclem6  31244  kelac1  31248  gicabl  31288  rgspnid  31362  itgpowd  31423  arearect  31424  areaquad  31425  nzss  31463  lhe4.4ex1a  31475  dvsconst  31476  dvsid  31477  dvsef  31478  dvconstbi  31480  binomcxplemnn0  31495  cnopn  31676  evthiccabs  31768  fprodclf  31834  islptre  31864  cncfshift  31915  addccncf2  31917  fsumcncf  31919  cncfperiod  31920  negcncfg  31922  cncfcompt  31924  ioccncflimc  31927  cncfuni  31928  icccncfext  31929  cncficcgt0  31930  icocncflimc  31931  cncfiooicclem1  31935  cncfiooicc  31936  cncfiooiccre  31937  cxpcncf2  31942  fprodcncf  31943  dvcosre  31945  dvcnre  31950  fperdvper  31954  dvmptresicc  31955  dvmptfprod  31981  itgsinexplem1  31991  itgcoscmulx  32007  ibliooicc  32009  itgsincmulx  32012  itgsubsticclem  32013  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  dirkeritg  32123  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem16  32144  fourierdlem18  32146  fourierdlem21  32149  fourierdlem22  32150  fourierdlem23  32151  fourierdlem32  32160  fourierdlem33  32161  fourierdlem39  32167  fourierdlem40  32168  fourierdlem57  32185  fourierdlem58  32186  fourierdlem59  32187  fourierdlem62  32190  fourierdlem68  32196  fourierdlem72  32200  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem83  32211  fourierdlem84  32212  fourierdlem85  32213  fourierdlem88  32216  fourierdlem93  32221  fourierdlem94  32222  fourierdlem95  32223  fourierdlem97  32225  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  fouriercn  32254  etransclem18  32274  etransclem22  32278  etransclem34  32290  etransclem46  32302  etransclem47  32303  funresfunco  32449  submgmid  32853  rnghmsscmap2  33035  rhmsscmap2  33081  srhmsubc  33138  fldhmsubc  33146  srhmsubcALTV  33157  fldhmsubcALTV  33165  elbigolo1  33432  onfrALTlem3  33710  onfrALTlem3VD  34088  bnj1253  34474  bj-rabtr  34898  bj-rabtrAUTO  34900  atpsubN  35874  pol1N  36031  1psubclN  36065  cdlemefrs32fva  36523  dia2dimlem13  37200  dibord  37283  dochvalr  37481  hdmapevec  37962  relexp0a  38223  corcltrcl  38231  wnefimgd  38426  wfximgfd  38431  extoimad  38433  funfvima2d  38438
  Copyright terms: Public domain W3C validator