Metamath Proof Explorer


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 ‘ 𝑆 ) ∈ 𝑆 )