Theorem undefnel

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

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

Proof

Step	Hyp	Ref	Expression
1		undefnel2	$$⊢S\in V\to \neg \mathrm{Undef}\left(S\right)\in S$$
2		df-nel	$$⊢\mathrm{Undef}\left(S\right)\notin S\leftrightarrow \neg \mathrm{Undef}\left(S\right)\in S$$
3	1 2	sylibr	$$⊢S\in V\to \mathrm{Undef}\left(S\right)\notin S$$