Definition df-base 16841

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 16843 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 16840	. 2 class Base
2		c1 10803	. . 3 class 1
3	2	cslot 16810	. 2 class Slot 1
4	1, 3	wceq 1539	1 wff Base = Slot 1

This definition is referenced by:  baseval  16842  baseid  16843  basendx  16849  basendxnnOLD  16851  1strwunOLD  16859  ressval3dOLD  16883  wunressOLD  16887  basendxnplusgndxOLD  16919  basendxnmulrndxOLD  16932  slotsbhcdifOLD  17045  wunfuncOLD  17531  wunnatOLD  17589  catcoppcclOLD  17749  catcfucclOLD  17751  estrreslem1OLD  17770  catcxpcclOLD  17841  oppgbasOLD  18872  symgvalstructOLD  18920  mgpbasOLD  19642  opprbasOLD  19785  rmodislmodOLD  20107  srabaseOLD  20357  zlmbasOLD  20633  znbas2OLD  20657  opsrbasOLD  21163  tngbasOLD  23705  ttgbasOLD  27144  baseltedgfOLD  27267  resvbasOLD  31435  hlhilsbaseOLD  39882  mnringbasedOLD  41719