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	⊢ SSet = ( ( V × V ) ∖ ran ( E ⊗ ( V ∖ E ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csset	⊢ SSet
1		cvv	⊢ V
2	1 1	cxp	⊢ ( V × V )
3		cep	⊢ E
4	1 3	cdif	⊢ ( V ∖ E )
5	3 4	ctxp	⊢ ( E ⊗ ( V ∖ E ) )
6	5	crn	⊢ ran ( E ⊗ ( V ∖ E ) )
7	2 6	cdif	⊢ ( ( V × V ) ∖ ran ( E ⊗ ( V ∖ E ) ) )
8	0 7	wceq	⊢ SSet = ( ( V × V ) ∖ ran ( E ⊗ ( V ∖ E ) ) )