Description: Define the undefined value function, whose value at set s is guaranteed not to be a member of s (see pwuninel ). (Contributed by NM, 15-Sep-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-undef | |- Undef = ( s e. _V |-> ~P U. s ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cund | |- Undef |
|
| 1 | vs | |- s |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- s |
| 4 | 3 | cuni | |- U. s |
| 5 | 4 | cpw | |- ~P U. s |
| 6 | 1 2 5 | cmpt | |- ( s e. _V |-> ~P U. s ) |
| 7 | 0 6 | wceq | |- Undef = ( s e. _V |-> ~P U. s ) |