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 16227
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 16221 . 2 class Base
2 c1 10252 . . 3 class 1
32cslot 16220 . 2 class Slot 1
41, 3wceq 1658 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  16241  base0  16274  baseval  16280  baseid  16281  basendx  16285  basendxnn  16286  ressval3d  16299  ressval3dOLD  16300  wunress  16303  1strwun  16340  basendxnplusgndx  16347  basendxnmulrndx  16357  slotsbhcdif  16432  wunfunc  16910  wunnat  16967  catcoppccl  17109  catcfuccl  17110  bascnvimaeqv  17112  estrcbasbas  17122  estrreslem1  17128  catcxpccl  17199  oppgbas  18130  mgpbas  18848  opprbas  18982  rmodislmod  19286  srabase  19538  rlmscaf  19568  opsrbas  19838  ply1tmcl  20001  ply1scltm  20010  ply1sclf  20014  ply1scl0  20019  ply1scl1  20021  zlmbas  20225  znbas2  20246  tngbas  22814  nrgtrg  22863  ttgbas  26175  baseltedgf  26291  resvbas  30376  hlhilsbase  38013  ringcbasbas  42880  ringcbasbasALTV  42904
  Copyright terms: Public domain W3C validator