Definition df-undef

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 = ( 𝑠 ∈ V ↦ 𝒫 ∪ 𝑠 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cund	⊢ Undef
1		vs	⊢ 𝑠
2		cvv	⊢ V
3	1	cv	⊢ 𝑠
4	3	cuni	⊢ ∪ 𝑠
5	4	cpw	⊢ 𝒫 ∪ 𝑠
6	1 2 5	cmpt	⊢ ( 𝑠 ∈ V ↦ 𝒫 ∪ 𝑠 )
7	0 6	wceq	⊢ Undef = ( 𝑠 ∈ V ↦ 𝒫 ∪ 𝑠 )