Definition df-undef 7399

Description: Define the undefined value function, whose value at set s is guaranteed not to be a member of s (see pwuninel 7401). (Contributed by NM, 15-Sep-2011.)

Assertion

Ref	Expression
df-undef	|- Undef = ( s e. _V |-> ~P U. s )

Detailed syntax breakdown of Definition df-undef

Step	Hyp	Ref	Expression
1		cund 7398	. 2 class Undef
2		vs	. . 3 setvar s
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class s
5	4	cuni 4436	. . . 4 class U. s
6	5	cpw 4158	. . 3 class ~P U. s
7	2, 3, 6	cmpt 4729	. 2 class ( s e. _V |-> ~P U. s )
8	1, 7	wceq 1483	1 wff Undef = ( s e. _V |-> ~P U. s )

This definition is referenced by:  undefval  7402