Theorem iota2

Description: The unique element such that ph . (Contributed by Jeff Madsen, 1-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypothesis	iota2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	iota2	$$⊢\left(A\in B\wedge \exists !x\phi \right)\to \left(\psi \leftrightarrow \left(\iota x|\phi \right)=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		iota2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		elex	$$⊢A\in B\to A\in \mathrm{V}$$
3		simpl	$$⊢\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\to A\in \mathrm{V}$$
4		simpr	$$⊢\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\to \exists !x\phi$$
5	1	adantl	$$⊢\left(\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
6		nfv	$$⊢ℲxA\in \mathrm{V}$$
7		nfeu1	$$⊢Ⅎx\exists !x\phi$$
8	6 7	nfan	$$⊢Ⅎx\left(A\in \mathrm{V}\wedge \exists !x\phi \right)$$
9		nfvd	$$⊢\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\to Ⅎx\psi$$
10		nfcvd	$$⊢\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\to \underset{\_}{Ⅎ}xA$$
11	3 4 5 8 9 10	iota2df	$$⊢\left(A\in \mathrm{V}\wedge \exists !x\phi \right)\to \left(\psi \leftrightarrow \left(\iota x|\phi \right)=A\right)$$
12	2 11	sylan	$$⊢\left(A\in B\wedge \exists !x\phi \right)\to \left(\psi \leftrightarrow \left(\iota x|\phi \right)=A\right)$$