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

Metamath Proof Explorer

Theorem undefne0

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

		Ref	Expression
	Assertion	undefne0	$⊢ S \in V \to Undef (S) \neq \emptyset$

Step	Hyp	Ref	Expression
1		undefval	$⊢ S \in V \to Undef (S) = 𝒫 ⋃ S$
2		pwne0	$⊢ 𝒫 ⋃ S \neq \emptyset$
3	2	a1i	$⊢ S \in V \to 𝒫 ⋃ S \neq \emptyset$
4	1 3	eqnetrd	$⊢ S \in V \to Undef (S) \neq \emptyset$