Theorem iota1

Description: Property of iota. (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Assertion	iota1	$$⊢\exists !x\phi \to \left(\phi \leftrightarrow \left(\iota x|\phi \right)=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		eu6	$$⊢\exists !x\phi \leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$
2		sp	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\phi \leftrightarrow x=z\right)$$
3		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\iota x|\phi \right)=z$$
4	3	eqeq2d	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(x=\left(\iota x|\phi \right)\leftrightarrow x=z\right)$$
5	2 4	bitr4d	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\phi \leftrightarrow x=\left(\iota x|\phi \right)\right)$$
6		eqcom	$$⊢x=\left(\iota x|\phi \right)\leftrightarrow \left(\iota x|\phi \right)=x$$
7	5 6	bitrdi	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\phi \leftrightarrow \left(\iota x|\phi \right)=x\right)$$
8	7	exlimiv	$$⊢\exists z\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\phi \leftrightarrow \left(\iota x|\phi \right)=x\right)$$
9	1 8	sylbi	$$⊢\exists !x\phi \to \left(\phi \leftrightarrow \left(\iota x|\phi \right)=x\right)$$