Theorem iotauni

Description: Equivalence between two different forms of iota . (Contributed by Andrew Salmon, 12-Jul-2011)

	Ref	Expression
Assertion	iotauni	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eu6	$$⊢\exists !x\phi \leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$
2		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\iota x|\phi \right)=z$$
3		uniabio	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \bigcup \left\{x|\phi \right\}=z$$
4	2 3	eqtr4d	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$
5	4	exlimiv	$$⊢\exists z\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$
6	1 5	sylbi	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$