Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-base Structured version   Visualization version   GIF version

Definition df-base 16483
 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 16477 . 2 class Base
2 c1 10529 . . 3 class 1
32cslot 16476 . 2 class Slot 1
41, 3wceq 1538 1 wff Base = Slot 1
 Colors of variables: wff setvar class This definition is referenced by:  basfn  16497  base0  16530  baseval  16536  baseid  16537  basendx  16541  basendxnn  16542  ressval3d  16555  wunress  16558  1strwun  16595  basendxnplusgndx  16602  basendxnmulrndx  16612  slotsbhcdif  16687  wunfunc  17163  wunnat  17220  catcoppccl  17362  catcfuccl  17363  estrcbasbas  17375  estrreslem1  17381  catcxpccl  17451  oppgbas  18474  symgvalstruct  18520  mgpbas  19241  opprbas  19378  rmodislmod  19698  srabase  19946  rlmscaf  19977  zlmbas  20215  znbas2  20235  opsrbas  20722  ply1tmcl  20908  ply1scltm  20917  ply1sclf  20921  ply1scl0  20926  ply1scl1  20928  tngbas  23254  nrgtrg  23303  ttgbas  26678  baseltedgf  26794  resvbas  30963  bj-endbase  34746  hlhilsbase  39251  mnringbased  40938  ringcbasbas  44673  ringcbasbasALTV  44697
 Copyright terms: Public domain W3C validator