Theorem iotain

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

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

Proof

Step	Hyp	Ref	Expression
1		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	intsn	$$⊢\bigcap \left\{y\right\}=y$$
4		abbi	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left\{x|\phi \right\}=\left\{x|x=y\right\}$$
5		df-sn	$$⊢\left\{y\right\}=\left\{x|x=y\right\}$$
6	4 5	eqtr4di	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left\{x|\phi \right\}=\left\{y\right\}$$
7	6	inteqd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcap \left\{x|\phi \right\}=\bigcap \left\{y\right\}$$
8		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
9	3 7 8	3eqtr4a	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcap \left\{x|\phi \right\}=\left(\iota x|\phi \right)$$
10	9	exlimiv	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcap \left\{x|\phi \right\}=\left(\iota x|\phi \right)$$
11	1 10	sylbi	$$⊢\exists !x\phi \to \bigcap \left\{x|\phi \right\}=\left(\iota x|\phi \right)$$