Definition df-singleton

Description: Define the singleton function. See brsingle for its value. (Contributed by Scott Fenton, 4-Apr-2014)

	Ref	Expression
Assertion	df-singleton	$$⊢\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csingle	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
1		cvv	$$class\mathrm{V}$$
2	1 1	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
3		cep	$$class\mathrm{E}$$
4	1 3	ctxp	$$class\left(\mathrm{V}\otimes \mathrm{E}\right)$$
5		cid	$$class\mathrm{I}$$
6	5 1	ctxp	$$class\left(\mathrm{I}\otimes \mathrm{V}\right)$$
7	4 6	csymdif	$$class\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$
8	7	crn	$$class\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$
9	2 8	cdif	$$class\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)$$
10	0 9	wceq	$$wff\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$$