Theorem undefne0

Description: The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018)

	Ref	Expression
Assertion	undefne0	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		undefval	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) = 𝒫 ∪ 𝑆 )
2		pwne0	⊢ 𝒫 ∪ 𝑆 ≠ ∅
3	2	a1i	⊢ ( 𝑆 ∈ 𝑉 → 𝒫 ∪ 𝑆 ≠ ∅ )
4	1 3	eqnetrd	⊢ ( 𝑆 ∈ 𝑉 → ( Undef ‘ 𝑆 ) ≠ ∅ )