Definition df-base 17188

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 17190 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 17187	. 2 class Base
2		c1 11147	. . 3 class 1
3	2	cslot 17157	. 2 class Slot 1
4	1, 3	wceq 1533	1 wff Base = Slot 1

This definition is referenced by:  baseval  17189  baseid  17190  basendx  17196  basendxnnOLD  17198  1strwunOLD  17208  ressval3dOLD  17235  wunressOLD  17239  basendxnplusgndxOLD  17271  basendxnmulrndxOLD  17284  slotsbhcdifOLD  17404  wunfuncOLD  17895  wunnatOLD  17954  catcoppcclOLD  18114  catcfucclOLD  18116  estrreslem1OLD  18135  catcxpcclOLD  18206  oppgbasOLD  19311  symgvalstructOLD  19359  mgpbasOLD  20088  opprbasOLD  20288  rmodislmodOLD  20821  srabaseOLD  21071  zlmbasOLD  21452  znbas2OLD  21478  opsrbasOLD  21997  tngbasOLD  24572  ttgbasOLD  28704  baseltedgfOLD  28827  resvbasOLD  33069  hlhilsbaseOLD  41446  mnringbasedOLD  43680