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	$$⊢\mathrm{Undef}=\left(s\in \mathrm{V}⟼𝒫\bigcup s\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cund	$$class\mathrm{Undef}$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvars$$
4	3	cuni	$$class\bigcup s$$
5	4	cpw	$$class𝒫\bigcup s$$
6	1 2 5	cmpt	$$class\left(s\in \mathrm{V}⟼𝒫\bigcup s\right)$$
7	0 6	wceq	$$wff\mathrm{Undef}=\left(s\in \mathrm{V}⟼𝒫\bigcup s\right)$$