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

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	$⊢ S \in V \to \neg Undef (S) \in S$

Step	Hyp	Ref	Expression
1		pwuninel	$⊢ \neg 𝒫 ⋃ S \in S$
2		undefval	$⊢ S \in V \to Undef (S) = 𝒫 ⋃ S$
3	2	eleq1d	$⊢ S \in V \to (Undef (S) \in S \leftrightarrow 𝒫 ⋃ S \in S)$
4	1 3	mtbiri	$⊢ S \in V \to \neg Undef (S) \in S$