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 17248
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 17250 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-base Base = Slot 1

Detailed syntax breakdown of Definition df-base
StepHypRef Expression
1 cbs 17247 . 2 class Base
2 c1 11156 . . 3 class 1
32cslot 17218 . 2 class Slot 1
41, 3wceq 1540 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  baseval  17249  baseid  17250  basendx  17256  wunressOLD  17296  basendxnmulrndxOLD  17340  slotsbhcdifOLD  17460  estrreslem1OLD  18182  symgvalstructOLD  19415  opprbasOLD  20342  srabaseOLD  21178  zlmbasOLD  21530  znbas2OLD  21556  opsrbasOLD  22070  tngbasOLD  24656  ttgbasOLD  28888  baseltedgfOLD  29011  resvbasOLD  33360  hlhilsbaseOLD  41943  sn-base0  42505  mnringbasedOLD  44231
  Copyright terms: Public domain W3C validator