Theorem undefne0

Description: The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018)

	Ref	Expression
Assertion	undefne0	$$⊢S\in V\to \mathrm{Undef}\left(S\right)\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		undefval	$$⊢S\in V\to \mathrm{Undef}\left(S\right)=𝒫\bigcup S$$
2		pwne0	$$⊢𝒫\bigcup S\ne \varnothing$$
3	2	a1i	$$⊢S\in V\to 𝒫\bigcup S\ne \varnothing$$
4	1 3	eqnetrd	$$⊢S\in V\to \mathrm{Undef}\left(S\right)\ne \varnothing$$