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

Proof

Step	Hyp	Ref	Expression
1		pwuninel	⊢ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆
2		undefval	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) = 𝒫 ∪ 𝑆 )
3	2	eleq1d	⊢ ( 𝑆 ∈ 𝑉 → ( ( Undef ‘ 𝑆 ) ∈ 𝑆 ↔ 𝒫 ∪ 𝑆 ∈ 𝑆 ) )
4	1 3	mtbiri	⊢ ( 𝑆 ∈ 𝑉 → ¬ ( Undef ‘ 𝑆 ) ∈ 𝑆 )