Definition df-base 16922

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 16924 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 16921	. 2 class Base
2		c1 10881	. . 3 class 1
3	2	cslot 16891	. 2 class Slot 1
4	1, 3	wceq 1539	1 wff Base = Slot 1

This definition is referenced by:  baseval  16923  baseid  16924  basendx  16930  basendxnnOLD  16932  1strwunOLD  16942  ressval3dOLD  16966  wunressOLD  16970  basendxnplusgndxOLD  17002  basendxnmulrndxOLD  17015  slotsbhcdifOLD  17135  wunfuncOLD  17624  wunnatOLD  17682  catcoppcclOLD  17842  catcfucclOLD  17844  estrreslem1OLD  17863  catcxpcclOLD  17934  oppgbasOLD  18966  symgvalstructOLD  19014  mgpbasOLD  19736  opprbasOLD  19879  rmodislmodOLD  20201  srabaseOLD  20451  zlmbasOLD  20730  znbas2OLD  20754  opsrbasOLD  21262  tngbasOLD  23808  ttgbasOLD  27250  baseltedgfOLD  27373  resvbasOLD  31542  hlhilsbaseOLD  39962  mnringbasedOLD  41837