![]() |
Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-singleton | Structured version Visualization version GIF version |
Description: Define the singleton function. See brsingle 35566 for its value. (Contributed by Scott Fenton, 4-Apr-2014.) |
Ref | Expression |
---|---|
df-singleton | ⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csingle 35487 | . 2 class Singleton | |
2 | cvv 3463 | . . . 4 class V | |
3 | 2, 2 | cxp 5671 | . . 3 class (V × V) |
4 | cep 5576 | . . . . . 6 class E | |
5 | 2, 4 | ctxp 35479 | . . . . 5 class (V ⊗ E ) |
6 | cid 5570 | . . . . . 6 class I | |
7 | 6, 2 | ctxp 35479 | . . . . 5 class ( I ⊗ V) |
8 | 5, 7 | csymdif 4237 | . . . 4 class ((V ⊗ E ) △ ( I ⊗ V)) |
9 | 8 | crn 5674 | . . 3 class ran ((V ⊗ E ) △ ( I ⊗ V)) |
10 | 3, 9 | cdif 3938 | . 2 class ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) |
11 | 1, 10 | wceq 1533 | 1 wff Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) |
Colors of variables: wff setvar class |
This definition is referenced by: brsingle 35566 fnsingle 35568 |
Copyright terms: Public domain | W3C validator |