Definition df-domain

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdomain	⊢ Domain
1		c1st	⊢ 1st
2		cvv	⊢ V
3	2 2	cxp	⊢ ( V × V )
4	1 3	cres	⊢ ( 1st ↾ ( V × V ) )
5	4	cimage	⊢ Image ( 1st ↾ ( V × V ) )
6	0 5	wceq	⊢ Domain = Image ( 1st ↾ ( V × V ) )