Theorem undefnel2

Description: The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Assertion	undefnel2	$$⊢S\in V\to \neg \mathrm{Undef}\left(S\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		pwuninel	$$⊢\neg 𝒫\bigcup S\in S$$
2		undefval	$$⊢S\in V\to \mathrm{Undef}\left(S\right)=𝒫\bigcup S$$
3	2	eleq1d	$$⊢S\in V\to \left(\mathrm{Undef}\left(S\right)\in S\leftrightarrow 𝒫\bigcup S\in S\right)$$
4	1 3	mtbiri	$$⊢S\in V\to \neg \mathrm{Undef}\left(S\right)\in S$$