Definition df-base 17245

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 17247 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 17244	. 2 class Base
2		c1 11153	. . 3 class 1
3	2	cslot 17214	. 2 class Slot 1
4	1, 3	wceq 1536	1 wff Base = Slot 1

This definition is referenced by:  baseval  17246  baseid  17247  basendx  17253  basendxnnOLD  17255  1strwunOLD  17265  ressval3dOLD  17292  wunressOLD  17296  basendxnplusgndxOLD  17328  basendxnmulrndxOLD  17341  slotsbhcdifOLD  17461  wunfuncOLD  17952  wunnatOLD  18011  catcoppcclOLD  18171  catcfucclOLD  18173  estrreslem1OLD  18192  catcxpcclOLD  18263  oppgbasOLD  19383  symgvalstructOLD  19429  mgpbasOLD  20158  opprbasOLD  20358  rmodislmodOLD  20945  srabaseOLD  21195  zlmbasOLD  21547  znbas2OLD  21573  opsrbasOLD  22087  tngbasOLD  24671  ttgbasOLD  28902  baseltedgfOLD  29025  resvbasOLD  33339  hlhilsbaseOLD  41923  sn-base0  42481  mnringbasedOLD  44207