df-domain - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-domain		Structured version Visualization version GIF version

Definition df-domain 31143

Description: Define the domain function. See brdomain 31210 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)

**Assertion**
Ref	Expression
df-domain	⊢ Domain = Image(1^st ↾ (V × V))

**Detailed syntax breakdown of Definition df-domain**
Step	Hyp	Ref	Expression
1		cdomain 31119	. 2 class Domain
2		c1st 7057	. . . 4 class 1^st
3		cvv 3173	. . . . 5 class V
4	3, 3	cxp 5036	. . . 4 class (V × V)
5	2, 4	cres 5040	. . 3 class (1^st ↾ (V × V))
6	5	cimage 31116	. 2 class Image(1^st ↾ (V × V))
7	1, 6	wceq 1475	1 wff Domain = Image(1^st ↾ (V × V))

Colors of variables: wff setvar class

This definition is referenced by: brdomain 31210