Definition df-undef 8073

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

Assertion

Ref	Expression
df-undef	⊢ Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠)

Detailed syntax breakdown of Definition df-undef

Step	Hyp	Ref	Expression
1		cund 8072	. 2 class Undef
2		vs	. . 3 setvar 𝑠
3		cvv 3430	. . 3 class V
4	2	cv 1540	. . . . 5 class 𝑠
5	4	cuni 4844	. . . 4 class ∪ 𝑠
6	5	cpw 4538	. . 3 class 𝒫 ∪ 𝑠
7	2, 3, 6	cmpt 5161	. 2 class (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠)
8	1, 7	wceq 1541	1 wff Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠)

This definition is referenced by:  undefval  8076