Definition df-sset

Description: Define the subset class. For the value, see brsset . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-sset	$$⊢\mathrm{𝖲𝖲𝖾𝗍}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csset	$$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	cdif	$$class\left(\mathrm{V}\setminus \mathrm{E}\right)$$
5	3 4	ctxp	$$class\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$$
6	5	crn	$$class\mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$$
7	2 6	cdif	$$class\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\right)$$
8	0 7	wceq	$$wff\mathrm{𝖲𝖲𝖾𝗍}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$$