Metamath Proof Explorer


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 𝖲𝖲𝖾𝗍 = V × V ran E V E

Detailed syntax breakdown

Step Hyp Ref Expression
0 csset class 𝖲𝖲𝖾𝗍
1 cvv class V
2 1 1 cxp class V × V
3 cep class E
4 1 3 cdif class V E
5 3 4 ctxp class E V E
6 5 crn class ran E V E
7 2 6 cdif class V × V ran E V E
8 0 7 wceq wff 𝖲𝖲𝖾𝗍 = V × V ran E V E