Definition df-base 17248

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 17250 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 17247	. 2 class Base
2		c1 11156	. . 3 class 1
3	2	cslot 17218	. 2 class Slot 1
4	1, 3	wceq 1540	1 wff Base = Slot 1

This definition is referenced by:  baseval  17249  baseid  17250  basendx  17256  wunressOLD  17296  basendxnmulrndxOLD  17340  slotsbhcdifOLD  17460  estrreslem1OLD  18182  symgvalstructOLD  19415  opprbasOLD  20342  srabaseOLD  21178  zlmbasOLD  21530  znbas2OLD  21556  opsrbasOLD  22070  tngbasOLD  24656  ttgbasOLD  28888  baseltedgfOLD  29011  resvbasOLD  33360  hlhilsbaseOLD  41943  sn-base0  42505  mnringbasedOLD  44231