Definition df-sset 31963

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

Assertion

Ref	Expression
df-sset	|- SSet = ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) )

Detailed syntax breakdown of Definition df-sset

Step	Hyp	Ref	Expression
1		csset 31939	. 2 class SSet
2		cvv 3200	. . . 4 class _V
3	2, 2	cxp 5112	. . 3 class ( _V X. _V )
4		cep 5028	. . . . 5 class _E
5	2, 4	cdif 3571	. . . . 5 class ( _V \ _E )
6	4, 5	ctxp 31937	. . . 4 class ( _E (x) ( _V \ _E ) )
7	6	crn 5115	. . 3 class ran ( _E (x) ( _V \ _E ) )
8	3, 7	cdif 3571	. 2 class ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) )
9	1, 8	wceq 1483	1 wff SSet = ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) )

This definition is referenced by:  relsset  31995  brsset  31996