Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sset Structured version   Visualization version   GIF version

Definition df-sset 32088
Description: Define the subset class. For the value, see brsset 32121. (Contributed by Scott Fenton, 31-Mar-2012.)
Assertion
Ref Expression
df-sset SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))

Detailed syntax breakdown of Definition df-sset
StepHypRef Expression
1 csset 32064 . 2 class SSet
2 cvv 3231 . . . 4 class V
32, 2cxp 5141 . . 3 class (V × V)
4 cep 5057 . . . . 5 class E
52, 4cdif 3604 . . . . 5 class (V ∖ E )
64, 5ctxp 32062 . . . 4 class ( E ⊗ (V ∖ E ))
76crn 5144 . . 3 class ran ( E ⊗ (V ∖ E ))
83, 7cdif 3604 . 2 class ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
91, 8wceq 1523 1 wff SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Colors of variables: wff setvar class
This definition is referenced by:  relsset  32120  brsset  32121
  Copyright terms: Public domain W3C validator