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	$$⊢\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdomain	$$class\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}$$
1		c1st	$$class{1}^{st}$$
2		cvv	$$class\mathrm{V}$$
3	2 2	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
4	1 3	cres	$$class\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
5	4	cimage	$$class\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
6	0 5	wceq	$$wff\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$