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

Metamath Proof Explorer

Theorem riotaund

Description: Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 13-Sep-2018)

		Ref	Expression
	Assertion	riotaund	$⊢ \neg \exists! x \in A φ \to (ι x \in A \| φ) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
2		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
3		iotanul	$⊢ \neg \exists! x (x \in A \land φ) \to (ι x \| (x \in A \land φ)) = \emptyset$
4	2 3	sylnbi	$⊢ \neg \exists! x \in A φ \to (ι x \| (x \in A \land φ)) = \emptyset$
5	1 4	eqtrid	$⊢ \neg \exists! x \in A φ \to (ι x \in A \| φ) = \emptyset$