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	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) ∉ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		undefnel2	⊢ ( 𝑆 ∈ 𝑉 → ¬ ( Undef ‘ 𝑆 ) ∈ 𝑆 )
2		df-nel	⊢ ( ( Undef ‘ 𝑆 ) ∉ 𝑆 ↔ ¬ ( Undef ‘ 𝑆 ) ∈ 𝑆 )
3	1 2	sylibr	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) ∉ 𝑆 )