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

Step	Hyp	Ref	Expression
1		cbs 16312	. 2 class Base
2		c1 10384	. . 3 class 1
3	2	cslot 16311	. 2 class Slot 1
4	1, 3	wceq 1522	1 wff Base = Slot 1

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