This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (s \in V ⟼ 𝒫 ⋃ s)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cund	$class Undef$
1		vs	$setvar s$
2		cvv	$class V$
3	1	cv	$setvar s$
4	3	cuni	$class ⋃ s$
5	4	cpw	$class 𝒫 ⋃ s$
6	1 2 5	cmpt	$class (s \in V ⟼ 𝒫 ⋃ s)$
7	0 6	wceq	$wff Undef = (s \in V ⟼ 𝒫 ⋃ s)$