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 16761
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 16760 . 2 class Base
2 c1 10730 . . 3 class 1
32cslot 16734 . 2 class Slot 1
41, 3wceq 1543 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  baseval  16762  baseid  16763  basendx  16769  basendxnnOLD  16771  1strwun  16777  ressval3d  16798  wunress  16801  basendxnplusgndx  16830  basendxnmulrndx  16839  slotsbhcdif  16922  wunfuncOLD  17406  wunnatOLD  17464  catcoppcclOLD  17624  catcfucclOLD  17626  estrreslem1  17644  catcxpcclOLD  17715  oppgbas  18743  symgvalstruct  18789  mgpbas  19510  opprbas  19647  rmodislmod  19967  srabase  20215  rlmscaf  20246  zlmbas  20484  znbas2  20504  opsrbas  21007  ply1tmcl  21193  ply1scltm  21202  ply1sclf  21206  ply1scl0  21211  ply1scl1  21213  tngbas  23539  nrgtrg  23588  ttgbas  26968  baseltedgf  27085  resvbas  31250  bj-endbase  35221  hlhilsbase  39690  mnringbased  41506  ringcbasbas  45265  ringcbasbasALTV  45289
  Copyright terms: Public domain W3C validator