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

Proof

Step	Hyp	Ref	Expression
1		df-undef	$$⊢\mathrm{Undef}=\left(s\in \mathrm{V}⟼𝒫\bigcup s\right)$$
2		unieq	$$⊢s=S\to \bigcup s=\bigcup S$$
3	2	pweqd	$$⊢s=S\to 𝒫\bigcup s=𝒫\bigcup S$$
4		elex	$$⊢S\in V\to S\in \mathrm{V}$$
5		uniexg	$$⊢S\in V\to \bigcup S\in \mathrm{V}$$
6	5	pwexd	$$⊢S\in V\to 𝒫\bigcup S\in \mathrm{V}$$
7	1 3 4 6	fvmptd3	$$⊢S\in V\to \mathrm{Undef}\left(S\right)=𝒫\bigcup S$$