Definition df-range 33331

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

Assertion

Ref	Expression
df-range	⊢ Range = Image(2nd ↾ (V × V))

Detailed syntax breakdown of Definition df-range

Step	Hyp	Ref	Expression
1		crange 33307	. 2 class Range
2		c2nd 7690	. . . 4 class 2nd
3		cvv 3496	. . . . 5 class V
4	3, 3	cxp 5555	. . . 4 class (V × V)
5	2, 4	cres 5559	. . 3 class (2nd ↾ (V × V))
6	5	cimage 33303	. 2 class Image(2nd ↾ (V × V))
7	1, 6	wceq 1537	1 wff Range = Image(2nd ↾ (V × V))

This definition is referenced by:  brrange  33397