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	$$⊢\mathrm{𝖱𝖺𝗇𝗀𝖾}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crange	$$class\mathrm{𝖱𝖺𝗇𝗀𝖾}$$
1		c2nd	$$class{2}^{nd}$$
2		cvv	$$class\mathrm{V}$$
3	2 2	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
4	1 3	cres	$$class\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
5	4	cimage	$$class\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
6	0 5	wceq	$$wff\mathrm{𝖱𝖺𝗇𝗀𝖾}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$