Definition df-base 16227

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

Step	Hyp	Ref	Expression
1		cbs 16221	. 2 class Base
2		c1 10252	. . 3 class 1
3	2	cslot 16220	. 2 class Slot 1
4	1, 3	wceq 1658	1 wff Base = Slot 1

This definition is referenced by:  basfn  16241  base0  16274  baseval  16280  baseid  16281  basendx  16285  basendxnn  16286  ressval3d  16299  ressval3dOLD  16300  wunress  16303  1strwun  16340  basendxnplusgndx  16347  basendxnmulrndx  16357  slotsbhcdif  16432  wunfunc  16910  wunnat  16967  catcoppccl  17109  catcfuccl  17110  bascnvimaeqv  17112  estrcbasbas  17122  estrreslem1  17128  catcxpccl  17199  oppgbas  18130  mgpbas  18848  opprbas  18982  rmodislmod  19286  srabase  19538  rlmscaf  19568  opsrbas  19838  ply1tmcl  20001  ply1scltm  20010  ply1sclf  20014  ply1scl0  20019  ply1scl1  20021  zlmbas  20225  znbas2  20246  tngbas  22814  nrgtrg  22863  ttgbas  26175  baseltedgf  26291  resvbas  30376  hlhilsbase  38013  ringcbasbas  42880  ringcbasbasALTV  42904