This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑆 ) = 𝒫 ∪ 𝑆 )