Metamath Proof Explorer


Theorem undefval

Description: Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel instead. (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion undefval ( 𝑆𝑉 → ( Undef ‘ 𝑆 ) = 𝒫 𝑆 )

Proof

Step Hyp Ref Expression
1 df-undef Undef = ( 𝑠 ∈ V ↦ 𝒫 𝑠 )
2 unieq ( 𝑠 = 𝑆 𝑠 = 𝑆 )
3 2 pweqd ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
4 elex ( 𝑆𝑉𝑆 ∈ V )
5 uniexg ( 𝑆𝑉 𝑆 ∈ V )
6 5 pwexd ( 𝑆𝑉 → 𝒫 𝑆 ∈ V )
7 1 3 4 6 fvmptd3 ( 𝑆𝑉 → ( Undef ‘ 𝑆 ) = 𝒫 𝑆 )