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 17188
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.) Use its index-independent form baseid 17190 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-base Base = Slot 1

Detailed syntax breakdown of Definition df-base
StepHypRef Expression
1 cbs 17187 . 2 class Base
2 c1 11147 . . 3 class 1
32cslot 17157 . 2 class Slot 1
41, 3wceq 1533 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  baseval  17189  baseid  17190  basendx  17196  basendxnnOLD  17198  1strwunOLD  17208  ressval3dOLD  17235  wunressOLD  17239  basendxnplusgndxOLD  17271  basendxnmulrndxOLD  17284  slotsbhcdifOLD  17404  wunfuncOLD  17895  wunnatOLD  17954  catcoppcclOLD  18114  catcfucclOLD  18116  estrreslem1OLD  18135  catcxpcclOLD  18206  oppgbasOLD  19311  symgvalstructOLD  19359  mgpbasOLD  20088  opprbasOLD  20288  rmodislmodOLD  20821  srabaseOLD  21071  zlmbasOLD  21452  znbas2OLD  21478  opsrbasOLD  21997  tngbasOLD  24572  ttgbasOLD  28704  baseltedgfOLD  28827  resvbasOLD  33069  hlhilsbaseOLD  41446  mnringbasedOLD  43680
  Copyright terms: Public domain W3C validator