Definition df-base 16489

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 16483	. 2 class Base
2		c1 10538	. . 3 class 1
3	2	cslot 16482	. 2 class Slot 1
4	1, 3	wceq 1537	1 wff Base = Slot 1

This definition is referenced by:  basfn  16503  base0  16536  baseval  16542  baseid  16543  basendx  16547  basendxnn  16548  ressval3d  16561  wunress  16564  1strwun  16601  basendxnplusgndx  16608  basendxnmulrndx  16618  slotsbhcdif  16693  wunfunc  17169  wunnat  17226  catcoppccl  17368  catcfuccl  17369  estrcbasbas  17381  estrreslem1  17387  catcxpccl  17457  oppgbas  18479  symgvalstruct  18525  mgpbas  19245  opprbas  19379  rmodislmod  19702  srabase  19950  rlmscaf  19981  opsrbas  20259  ply1tmcl  20440  ply1scltm  20449  ply1sclf  20453  ply1scl0  20458  ply1scl1  20460  zlmbas  20665  znbas2  20686  tngbas  23250  nrgtrg  23299  ttgbas  26663  baseltedgf  26779  resvbas  30905  bj-endbase  34600  hlhilsbase  39090  ringcbasbas  44354  ringcbasbasALTV  44378