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 16479
Description: Define the base set (also called underlying set, ground set, carrier set, or carrier) 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 16473 . 2 class Base
2 c1 10527 . . 3 class 1
32cslot 16472 . 2 class Slot 1
41, 3wceq 1528 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  16493  base0  16526  baseval  16532  baseid  16533  basendx  16537  basendxnn  16538  ressval3d  16551  wunress  16554  1strwun  16591  basendxnplusgndx  16598  basendxnmulrndx  16608  slotsbhcdif  16683  wunfunc  17159  wunnat  17216  catcoppccl  17358  catcfuccl  17359  estrcbasbas  17371  estrreslem1  17377  catcxpccl  17447  oppgbas  18419  mgpbas  19176  opprbas  19310  rmodislmod  19633  srabase  19881  rlmscaf  19911  opsrbas  20189  ply1tmcl  20370  ply1scltm  20379  ply1sclf  20383  ply1scl0  20388  ply1scl1  20390  zlmbas  20595  znbas2  20616  tngbas  23179  nrgtrg  23228  ttgbas  26591  baseltedgf  26707  resvbas  30833  hlhilsbase  38957  ringcbasbas  44203  ringcbasbasALTV  44227
  Copyright terms: Public domain W3C validator