Definition df-base 17259

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 17261 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 17258	. 2 class Base
2		c1 11185	. . 3 class 1
3	2	cslot 17228	. 2 class Slot 1
4	1, 3	wceq 1537	1 wff Base = Slot 1

This definition is referenced by:  baseval  17260  baseid  17261  basendx  17267  basendxnnOLD  17269  1strwunOLD  17279  ressval3dOLD  17306  wunressOLD  17310  basendxnplusgndxOLD  17342  basendxnmulrndxOLD  17355  slotsbhcdifOLD  17475  wunfuncOLD  17966  wunnatOLD  18025  catcoppcclOLD  18185  catcfucclOLD  18187  estrreslem1OLD  18206  catcxpcclOLD  18277  oppgbasOLD  19393  symgvalstructOLD  19439  mgpbasOLD  20168  opprbasOLD  20368  rmodislmodOLD  20951  srabaseOLD  21201  zlmbasOLD  21553  znbas2OLD  21579  opsrbasOLD  22093  tngbasOLD  24677  ttgbasOLD  28906  baseltedgfOLD  29029  resvbasOLD  33325  hlhilsbaseOLD  41898  mnringbasedOLD  44181