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 16318
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 16312 . 2 class Base
2 c1 10384 . . 3 class 1
32cslot 16311 . 2 class Slot 1
41, 3wceq 1522 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  16332  base0  16365  baseval  16371  baseid  16372  basendx  16376  basendxnn  16377  ressval3d  16390  wunress  16393  1strwun  16430  basendxnplusgndx  16437  basendxnmulrndx  16447  slotsbhcdif  16522  wunfunc  16998  wunnat  17055  catcoppccl  17197  catcfuccl  17198  estrcbasbas  17210  estrreslem1  17216  catcxpccl  17286  oppgbas  18220  mgpbas  18935  opprbas  19069  rmodislmod  19392  srabase  19640  rlmscaf  19670  opsrbas  19946  ply1tmcl  20123  ply1scltm  20132  ply1sclf  20136  ply1scl0  20141  ply1scl1  20143  zlmbas  20347  znbas2  20368  tngbas  22933  nrgtrg  22982  ttgbas  26346  baseltedgf  26462  resvbas  30559  hlhilsbase  38606  ringcbasbas  43783  ringcbasbasALTV  43807
  Copyright terms: Public domain W3C validator