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

Metamath Proof Explorer

Theorem dfiota4

Description: The iota operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017) (Proof shortened by JJ, 28-Oct-2021)

		Ref	Expression
	Assertion	dfiota4	$⊢ (ι x \| φ) = if (\exists! x φ, ⋃ \{x \| φ\}, \emptyset)$

Step	Hyp	Ref	Expression
1		iotauni	$⊢ \exists! x φ \to (ι x \| φ) = ⋃ \{x \| φ\}$
2		iotanul	$⊢ \neg \exists! x φ \to (ι x \| φ) = \emptyset$
3		ifval	$⊢ (ι x \| φ) = if (\exists! x φ, ⋃ \{x \| φ\}, \emptyset) \leftrightarrow ((\exists! x φ \to (ι x \| φ) = ⋃ \{x \| φ\}) \land (\neg \exists! x φ \to (ι x \| φ) = \emptyset))$
4	1 2 3	mpbir2an	$⊢ (ι x \| φ) = if (\exists! x φ, ⋃ \{x \| φ\}, \emptyset)$