Definition df-base 17142

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 17144 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 17141	. 2 class Base
2		c1 11108	. . 3 class 1
3	2	cslot 17111	. 2 class Slot 1
4	1, 3	wceq 1542	1 wff Base = Slot 1

This definition is referenced by:  baseval  17143  baseid  17144  basendx  17150  basendxnnOLD  17152  1strwunOLD  17162  ressval3dOLD  17189  wunressOLD  17193  basendxnplusgndxOLD  17225  basendxnmulrndxOLD  17238  slotsbhcdifOLD  17358  wunfuncOLD  17847  wunnatOLD  17905  catcoppcclOLD  18065  catcfucclOLD  18067  estrreslem1OLD  18086  catcxpcclOLD  18157  oppgbasOLD  19212  symgvalstructOLD  19260  mgpbasOLD  19989  opprbasOLD  20151  rmodislmodOLD  20534  srabaseOLD  20786  zlmbasOLD  21061  znbas2OLD  21085  opsrbasOLD  21599  tngbasOLD  24144  ttgbasOLD  28121  baseltedgfOLD  28244  resvbasOLD  32437  hlhilsbaseOLD  40801  mnringbasedOLD  42957