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

Theorem ssid 3506
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 3491 1  |-  A  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802    C_ wss 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3466  df-ss 3473
This theorem is referenced by:  eqimssi  3541  eqimss2i  3542  nsspssun  3714  inv1  3795  disjpss  3860  difid  3879  pwidg  4007  elssuni  4261  unimax  4267  intmin  4288  rintn0  4403  sseliALT  4565  ordunidif  4913  xpss1  5098  xpss2  5099  residm  5292  resdm  5302  resmpt3  5311  ssrnres  5432  dffn3  5725  fdmrn  5733  fvreseq1  5970  fimacnv  6001  iunpw  6596  onsucuni  6645  tfisi  6675  fparlem3  6884  fparlem4  6885  funsssuppss  6925  suppofss1d  6936  suppofss2d  6937  tfrlem1  7044  tz7.48-2  7106  oaordi  7194  omwordi  7219  omass  7228  nnaordi  7266  nnmwordi  7283  fpmg  7443  ralxpmap  7467  boxcutc  7511  domss2  7675  0fin  7746  en1eqsn  7748  findcard2d  7761  fimax2g  7765  domunfican  7792  pwfi  7814  fissuni  7824  fipreima  7825  fsuppmptif  7858  fsuppco2  7861  fsuppcor  7862  mapfienlem1  7863  mapfienlem2  7864  wofib  7970  wemapso  7976  sucprcregOLD  8026  noinfep  8076  noinfepOLD  8077  cantnfval2  8088  cantnfp1lem3  8099  cantnflem1  8108  cantnfval2OLD  8118  cantnfp1lem3OLD  8125  tcidm  8177  tc0  8178  r1rankidb  8222  r1pw  8263  rankr1id  8280  scott0  8304  htalem  8314  xpomen  8393  infpwfien  8443  alephsmo  8483  dfac12lem3  8525  ackbij2lem4  8622  cflem  8626  cflecard  8633  cflim2  8643  cfslb  8646  fin4en1  8689  fin23lem13  8712  fin23lem15  8714  fin23lem36  8728  isf32lem1  8733  fin67  8775  dcomex  8827  zorn2lem4  8879  alephexp2  8956  fpwwe2lem13  9020  canthnumlem  9026  wunex2  9116  wuncidm  9124  eltsk2g  9129  axgroth6  9206  axgroth3  9209  xrsup  11971  expcl  12160  hashcard  12403  hashf1lem2  12481  lo1eq  13367  rlimeq  13368  serclim0  13376  isercolllem2  13464  isercoll  13466  summolem3  13512  isum  13517  fsumser  13528  fsumcl  13531  fsum2d  13562  fsumabs  13591  fsumrlim  13601  fsumo1  13602  fsumiun  13611  flo1  13642  eflt  13726  xpnnenOLD  13817  rpnnen2lem3  13824  rpnnen2lem5  13826  rpnnen2lem11  13832  rpnnen2  13833  rexpen  13835  eulerthlem2  14186  ressid  14566  ressinbas  14567  mremre  14875  yon11  15404  yon12  15405  yon2  15406  yonpropd  15408  oppcyon  15409  yonffth  15424  oduclatb  15645  ipopos  15661  fpwipodrs  15665  submid  15853  mulgnncl  16028  mulgnn0cl  16029  mulgcl  16030  subgid  16074  cntrnsg  16250  symggen  16366  sylow3lem5  16522  lsmss1  16555  lsmss2  16557  gsumzres  16785  gsumzcl2  16786  gsumzf1o  16788  gsumzresOLD  16789  gsumzclOLD  16790  gsumzf1oOLD  16791  gsumadd  16809  gsumaddOLD  16810  gsumzsplitOLD  16816  gsumzmhm  16828  gsumzmhmOLD  16829  gsumzoppg  16838  gsumzoppgOLD  16839  gsumzinvOLD  16841  gsumsubOLD  16846  gsum2dlem1  16868  gsum2dlem2  16869  gsum2d  16870  gsum2dOLD  16871  dprdfinv  16930  dprdfinvOLD  16937  dprdf1  16951  dmdprdsplitlem  16955  dmdprdsplitlemOLD  16956  dprd2db  16963  dpjidcl  16978  dpjidclOLD  16985  ablfac1eulem  16994  ablfac1eu  16995  ablfaclem2  17008  gsumdixpOLD  17128  gsumdixp  17129  subrgid  17302  lcomfsupOLD  17420  lcomfsupp  17421  lss1  17456  lbsextlem1  17675  rlmval2  17711  rlmbas  17712  rlmplusg  17713  rlm0  17714  rlmmulr  17716  rlmsca  17717  rlmsca2  17718  rlmvsca  17719  rlmtopn  17720  rlmds  17721  psrass1lem  17900  mplsubglem  17964  mpllsslem  17965  mplsubglemOLD  17966  mpllsslemOLD  17967  mplsubrglem  17971  mplsubrglemOLD  17972  mplcoe1  17998  mplcoe5  18002  mplbas2  18005  mplbas2OLD  18006  evlslem4OLD  18044  evlslem4  18045  psrbagev1  18048  psrbagev1OLD  18049  evlslem2  18051  ply1coeOLD  18209  znf1o  18460  zntoslem  18465  regsumsupp  18528  css0  18590  uvcresum  18694  frlmsslsp  18699  frlmsslspOLD  18700  frlmlbs  18701  frlmup1  18702  mamures  18762  mdetrsca2  18976  mdetrlin2  18979  mdetunilem5  18988  mdetunilem9  18992  smadiadetglem1  19043  smadiadetglem2  19044  pmatcollpw3  19155  cpmadumatpolylem2  19253  topopn  19285  fiinbas  19323  topbas  19344  topcld  19406  clstop  19440  ntrtop  19441  opnneissb  19485  opnssneib  19486  opnneiid  19497  neiptopuni  19501  neiptoptop  19502  maxlp  19518  isperf2  19523  restopn2  19548  restperf  19555  idcn  19628  cnconst2  19654  lmres  19671  rncmp  19766  fiuncmp  19774  cmpfi  19778  concn  19797  1stcelcls  19832  llyidm  19859  nllyidm  19860  toplly  19861  ssref  19883  refref  19884  kgentopon  19909  kgencn2  19928  ptpjpre1  19942  ptbasfi  19952  ptcld  19984  xkopt  20026  elqtop2  20072  qtopuni  20073  ptcmpfi  20184  fbssfi  20208  opnfbas  20213  filtop  20226  isfil2  20227  isfild  20229  fsubbas  20238  ssfg  20243  filssufilg  20282  ufileu  20290  imaelfm  20322  rnelfm  20324  fmfnfmlem4  20328  neiflim  20345  supnfcls  20391  fclscf  20396  flimfnfcls  20399  tsmsfbas  20496  utopbas  20608  xpsxmet  20753  xpsdsval  20754  xpsmet  20755  tmsxms  20859  tmsms  20860  imasf1oxms  20862  imasf1oms  20863  prdsxms  20903  prdsms  20904  tmsxpsval  20911  retopbas  21137  cnngp  21157  cnperf  21195  retopcon  21204  fsumcn  21244  abscncf  21275  recncf  21276  imcncf  21277  cjcncf  21278  mulc1cncf  21279  cncfcn1  21284  cncfmpt2f  21288  cncfmpt2ss  21289  addccncf  21290  cdivcncf  21291  negcncf  21292  negfcncf  21293  abscncfALT  21294  cnmpt2pc  21298  xrhmeo  21316  oprpiece1res1  21321  oprpiece1res2  21322  cnrehmeo  21323  iscau3  21587  caubl  21616  caublcls  21617  rrxcph  21694  rrxmval  21702  rrxdstprj1  21706  evthicc2  21742  ovolre  21806  volsuplem  21835  uniiccdif  21857  uniioovol  21858  uniiccvol  21859  uniioombllem3  21864  uniioombllem4  21865  uniioombllem5  21866  dyadmbllem  21878  volcn  21885  volivth  21886  itgfsum  22103  iblabslem  22104  iblabs  22105  bddmulibl  22115  cnlimc  22162  cnlimci  22163  dvres3  22187  dvres3a  22188  dvidlem  22189  dvcnp2  22193  dvcn  22194  dvnadd  22202  dvnres  22204  cpnord  22208  cpnres  22210  dvaddbr  22211  dvmulbr  22212  dvcmul  22217  dvcmulf  22218  dvcobr  22219  dvcjbr  22222  dvrec  22228  dvmptntr  22244  dvmptfsum  22246  dveflem  22250  dvef  22251  rolle  22261  dvlipcn  22265  c1liplem1  22267  dvgt0lem2  22274  dvivth  22281  lhop1lem  22284  dvfsumabs  22294  ftc1a  22308  ftc1cn  22314  ftc2  22315  deg1mul3le  22387  plyssc  22467  plyeq0  22478  coeeulem  22491  0dgr  22512  coemulc  22521  coe0  22522  coesub  22523  coe1termlem  22524  dgrmulc  22537  dgrsub  22538  dgrcolem1  22539  dgrcolem2  22540  dvnply2  22552  plycpn  22554  plyremlem  22569  fta1lem  22572  vieta1lem2  22576  aalioulem3  22599  dvntaylp  22635  taylthlem1  22637  taylthlem2  22638  ulmcn  22663  psercn  22690  pserdv  22693  abelth  22705  efcn  22707  efcvx  22713  pige3  22779  dvrelog  22887  logcn  22897  dvloglem  22898  dvlog  22901  dvlog2  22903  efopnlem2  22907  logccv  22913  cxpcn  22988  cxpcn2  22989  cxpcn3  22991  resqrtcn  22992  sqrtcn  22993  loglesqrt  23001  atancn  23136  rlimcnp3  23166  jensen  23187  ftalem3  23217  basellem2  23224  dchrfi  23399  dchrisumlema  23542  pntrsumo1  23619  pntrsumbnd  23620  pntlem3  23663  cusgrasizeindslem2  24343  efghgrpOLD  25244  sspid  25507  ssps  25512  helch  26030  hhssnv  26049  hhsssh  26054  shintcl  26117  chintcl  26119  shlesb1i  26173  omlsi  26191  chlejb1i  26263  chm0i  26277  chabs1  26303  chabs2  26304  spanun  26332  cmidi  26397  pjidmcoi  26965  csmdsymi  27122  sumdmdlem2  27207  dmdbr5ati  27210  mdcompli  27217  dmdcompli  27218  disjdifprg  27305  fcoinver  27329  xppreima  27356  xrinfm  27444  clatp0cl  27529  clatp1cl  27530  xrsmulgzz  27536  xrsp0  27539  xrsp1  27540  gsumle  27640  gsummpt2co  27641  gsumvsca1  27643  gsumvsca2  27644  reff  27712  locfinreflem  27713  pnfneige0  27803  esumsn  27942  esumcvg  27962  pwsiga  28000  sigagenid  28021  lgamgulmlem2  28442  cvmlift2lem6  28623  mrsubrn  28743  mrsubff1  28744  mrsub0  28746  mrsubccat  28748  mrsubcn  28749  elmrsubrn  28750  elmsubrn  28758  msubrn  28759  msubff1  28786  mthmpps  28812  relexpdm  28928  relexprn  28929  rtrclreclem.refl  28937  rtrclreclem.subset  28938  prodmolem3  29037  iprod  29042  iprodn0  29044  fprodss  29052  fprodcl  29056  fprod2d  29083  risefaccl  29109  fallfaccl  29110  trpredtr  29285  trpredpo  29290  wzel  29352  frrlem5c  29365  frrlem10  29370  imagesset  29575  ontgval  29868  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  ovoliunnfl  30028  voliunnfl  30030  volsupnfl  30031  mbfposadd  30034  ftc1cnnclem  30060  ftc1cnnc  30061  ftc1anc  30070  ftc2nc  30071  areacirclem2  30080  areacirclem3  30081  areacirclem4  30082  areacirc  30084  ivthALT  30125  fness  30139  fneref  30140  refssfne  30148  fnemeet1  30156  fnejoin2  30159  filnetlem2  30169  filnetlem4  30171  welb  30199  caures  30225  constcncf  30227  idcncf  30228  sub1cncf  30229  sub2cncf  30230  cnresima  30232  rngoidl  30393  ismrcd1  30602  ismrc  30605  incssnn0  30615  mzpclall  30631  rmydioph  30928  rmxdioph  30930  expdiophlem2  30936  expdioph  30937  aomclem6  30977  kelac1  30981  gicabl  31019  rgspnid  31094  itgpowd  31155  arearect  31156  areaquad  31157  nzss  31195  lhe4.4ex1a  31207  dvsconst  31208  dvsid  31209  dvsef  31210  dvconstbi  31212  cnopn  31390  evthiccabs  31465  islptre  31533  cncfshift  31583  addccncf2  31585  fsumcncf  31587  cncfperiod  31588  negcncfg  31590  cncfcompt  31592  ioccncflimc  31595  cncfuni  31596  icccncfext  31597  cncficcgt0  31598  icocncflimc  31599  cncfiooicclem1  31603  cncfiooicc  31604  cncfiooiccre  31605  dvcosre  31610  dvcnre  31615  fperdvper  31619  dvmptresicc  31620  itgsinexplem1  31642  itgcoscmulx  31658  ibliooicc  31660  itgsincmulx  31663  itgsubsticclem  31664  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  dirkeritg  31773  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem16  31794  fourierdlem18  31796  fourierdlem21  31799  fourierdlem22  31800  fourierdlem23  31801  fourierdlem32  31810  fourierdlem33  31811  fourierdlem39  31817  fourierdlem40  31818  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem62  31840  fourierdlem68  31846  fourierdlem72  31850  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem78  31856  fourierdlem83  31861  fourierdlem84  31862  fourierdlem85  31863  fourierdlem88  31866  fourierdlem93  31871  fourierdlem94  31872  fourierdlem95  31873  fourierdlem97  31875  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  fouriercn  31904  funresfunco  32048  submgmid  32319  rnghmsscmap2  32518  rhmsscmap2  32559  srhmsubc  32612  fldhmsubc  32620  srhmsubcOLD  32631  fldhmsubcOLD  32639  onfrALTlem3  33044  onfrALTlem3VD  33415  bnj1253  33801  bj-rabtr  34230  bj-rabtrAUTO  34232  atpsubN  35200  pol1N  35357  1psubclN  35391  cdlemefrs32fva  35849  dia2dimlem13  36526  dibord  36609  dochvalr  36807  hdmapevec  37288  xptrrel  37451  wnefimgd  37626  wfximgfd  37631  extoimad  37633  funfvima2d  37638
  Copyright terms: Public domain W3C validator