Definition df-range

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

	Ref	Expression
Assertion	df-range	|- Range = Image ( 2nd |` ( _V X. _V ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crange	|- Range
1		c2nd	|- 2nd
2		cvv	|- _V
3	2 2	cxp	|- ( _V X. _V )
4	1 3	cres	|- ( 2nd |` ( _V X. _V ) )
5	4	cimage	|- Image ( 2nd |` ( _V X. _V ) )
6	0 5	wceq	|- Range = Image ( 2nd |` ( _V X. _V ) )