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 16081
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 16075 . 2 class Base
2 c1 10229 . . 3 class 1
32cslot 16074 . 2 class Slot 1
41, 3wceq 1637 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  16095  base0  16130  baseval  16136  baseid  16137  basendx  16141  basendxnn  16142  ressval3d  16155  ressval3dOLD  16156  wunress  16159  1strwun  16200  basendxnplusgndx  16207  basendxnmulrndx  16217  slotsbhcdif  16292  wunfunc  16770  wunnat  16827  catcoppccl  16969  catcfuccl  16970  bascnvimaeqv  16972  estrcbasbas  16982  estrreslem1  16988  catcxpccl  17059  oppgbas  17989  mgpbas  18704  opprbas  18838  rmodislmod  19142  srabase  19394  rlmscaf  19424  opsrbas  19694  ply1tmcl  19857  ply1scltm  19866  ply1sclf  19870  ply1scl0  19875  ply1scl1  19877  zlmbas  20081  znbas2  20102  tngbas  22666  nrgtrg  22715  ttgbas  25981  baseltedgf  26096  basvtxvalOLD  26127  resvbas  30167  hlhilsbase  37725  ringcbasbas  42607  ringcbasbasALTV  42631
  Copyright terms: Public domain W3C validator