MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-base Structured version   Visualization version   GIF version

Definition df-base 16063
Description: Define the base set (also called underlying set or carrier set) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-base Base = Slot 1

Detailed syntax breakdown of Definition df-base
StepHypRef Expression
1 cbs 16057 . 2 class Base
2 c1 10127 . . 3 class 1
32cslot 16056 . 2 class Slot 1
41, 3wceq 1630 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  16077  base0  16112  baseval  16118  baseid  16119  basendx  16123  basendxnn  16124  ressval3d  16137  wunress  16140  1strwun  16182  basendxnplusgndx  16189  basendxnmulrndx  16199  slotsbhcdif  16280  wunfunc  16758  wunnat  16815  catcoppccl  16957  catcfuccl  16958  bascnvimaeqv  16960  estrcbasbas  16970  estrreslem1  16976  catcxpccl  17046  oppgbas  17979  mgpbas  18693  opprbas  18827  rmodislmod  19131  srabase  19378  rlmscaf  19408  opsrbas  19679  ply1tmcl  19842  ply1scltm  19851  ply1sclf  19855  ply1scl0  19860  ply1scl1  19862  zlmbas  20066  znbas2  20088  tngbas  22644  nrgtrg  22693  ttgbas  25954  baseltedgf  26069  basvtxvalOLD  26100  resvbas  30139  hlhilsbase  37731  ringcbasbas  42542  ringcbasbasALTV  42566
  Copyright terms: Public domain W3C validator