Definition df-base 16761

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.)

Assertion

Ref	Expression
df-base	⊢ Base = Slot 1

Detailed syntax breakdown of Definition df-base

Step	Hyp	Ref	Expression
1		cbs 16760	. 2 class Base
2		c1 10730	. . 3 class 1
3	2	cslot 16734	. 2 class Slot 1
4	1, 3	wceq 1543	1 wff Base = Slot 1

This definition is referenced by:  baseval  16762  baseid  16763  basendx  16769  basendxnnOLD  16771  1strwun  16777  ressval3d  16798  wunress  16801  basendxnplusgndx  16830  basendxnmulrndx  16839  slotsbhcdif  16922  wunfuncOLD  17406  wunnatOLD  17464  catcoppcclOLD  17624  catcfucclOLD  17626  estrreslem1  17644  catcxpcclOLD  17715  oppgbas  18743  symgvalstruct  18789  mgpbas  19510  opprbas  19647  rmodislmod  19967  srabase  20215  rlmscaf  20246  zlmbas  20484  znbas2  20504  opsrbas  21007  ply1tmcl  21193  ply1scltm  21202  ply1sclf  21206  ply1scl0  21211  ply1scl1  21213  tngbas  23539  nrgtrg  23588  ttgbas  26968  baseltedgf  27085  resvbas  31250  bj-endbase  35221  hlhilsbase  39690  mnringbased  41506  ringcbasbas  45265  ringcbasbasALTV  45289