Definition df-base 17011

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 17013 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 17010	. 2 class Base
2		c1 10974	. . 3 class 1
3	2	cslot 16980	. 2 class Slot 1
4	1, 3	wceq 1540	1 wff Base = Slot 1

This definition is referenced by:  baseval  17012  baseid  17013  basendx  17019  basendxnnOLD  17021  1strwunOLD  17031  ressval3dOLD  17055  wunressOLD  17059  basendxnplusgndxOLD  17091  basendxnmulrndxOLD  17104  slotsbhcdifOLD  17224  wunfuncOLD  17713  wunnatOLD  17771  catcoppcclOLD  17931  catcfucclOLD  17933  estrreslem1OLD  17952  catcxpcclOLD  18023  oppgbasOLD  19054  symgvalstructOLD  19102  mgpbasOLD  19823  opprbasOLD  19966  rmodislmodOLD  20299  srabaseOLD  20549  zlmbasOLD  20828  znbas2OLD  20852  opsrbasOLD  21360  tngbasOLD  23906  ttgbasOLD  27531  baseltedgfOLD  27654  resvbasOLD  31829  hlhilsbaseOLD  40260  mnringbasedOLD  42203