Definition df-undef 5769

Description: Define the undefined value function, whose value at set s is guaranteed not to be a member of s (see pwuninel 5762).

Assertion

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

Detailed syntax breakdown of Definition df-undef

Step	Hyp	Ref	Expression
1		cund 5767	. 2 class Undef
2		vs	. . 3 set s
3		cvv 2569	. . 3 class _V
4	2	cv 1614	. . . . 5 class s
5	4	cuni 3398	. . . 4 class U.s
6	5	cpw 3259	. . 3 class ~PU.s
7	2, 3, 6	cmpt 5136	. 2 class (s e. _V |-> ~PU.s)
8	1, 7	wceq 1615	1 wff Undef = (s e. _V |-> ~PU.s)

This definition is referenced by:  undefval 5770

Copyright terms: Public domain