Definition df-base 17151

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.) Use its index-independent form baseid 17153 instead. (New usage is discouraged.)

Assertion

Ref	Expression
df-base	⊢ Base = Slot 1

Detailed syntax breakdown of Definition df-base

Step	Hyp	Ref	Expression
1		cbs 17150	. 2 class Base
2		c1 11110	. . 3 class 1
3	2	cslot 17120	. 2 class Slot 1
4	1, 3	wceq 1533	1 wff Base = Slot 1

This definition is referenced by:  baseval  17152  baseid  17153  basendx  17159  basendxnnOLD  17161  1strwunOLD  17171  ressval3dOLD  17198  wunressOLD  17202  basendxnplusgndxOLD  17234  basendxnmulrndxOLD  17247  slotsbhcdifOLD  17367  wunfuncOLD  17858  wunnatOLD  17917  catcoppcclOLD  18077  catcfucclOLD  18079  estrreslem1OLD  18098  catcxpcclOLD  18169  oppgbasOLD  19266  symgvalstructOLD  19314  mgpbasOLD  20043  opprbasOLD  20241  rmodislmodOLD  20774  srabaseOLD  21024  zlmbasOLD  21401  znbas2OLD  21427  opsrbasOLD  21944  tngbasOLD  24502  ttgbasOLD  28634  baseltedgfOLD  28757  resvbasOLD  32950  hlhilsbaseOLD  41324  mnringbasedOLD  43529