Theorem undefval

Description: Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel instead. (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	undefval	|- ( S e. V -> ( Undef ` S ) = ~P U. S )

Proof

Step	Hyp	Ref	Expression
1		df-undef	|- Undef = ( s e. _V |-> ~P U. s )
2		unieq	|- ( s = S -> U. s = U. S )
3	2	pweqd	|- ( s = S -> ~P U. s = ~P U. S )
4		elex	|- ( S e. V -> S e. _V )
5		uniexg	|- ( S e. V -> U. S e. _V )
6	5	pwexd	|- ( S e. V -> ~P U. S e. _V )
7	1 3 4 6	fvmptd3	|- ( S e. V -> ( Undef ` S ) = ~P U. S )