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	$$⊢\left(\iota x|\phi \right)=if\left(\exists !x\phi ,\bigcup \left\{x|\phi \right\},\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		iotauni	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$
2		iotanul	$$⊢\neg \exists !x\phi \to \left(\iota x|\phi \right)=\varnothing$$
3		ifval	$$⊢\left(\iota x|\phi \right)=if\left(\exists !x\phi ,\bigcup \left\{x|\phi \right\},\varnothing \right)\leftrightarrow \left(\left(\exists !x\phi \to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}\right)\wedge \left(\neg \exists !x\phi \to \left(\iota x|\phi \right)=\varnothing \right)\right)$$
4	1 2 3	mpbir2an	$$⊢\left(\iota x|\phi \right)=if\left(\exists !x\phi ,\bigcup \left\{x|\phi \right\},\varnothing \right)$$