This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 ) ) ) |