Theorem iota5f

Description: A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017)

	Ref	Expression
Hypotheses	iota5f.1	$$⊢Ⅎx\phi$$
	iota5f.2	$$⊢\underset{\_}{Ⅎ}xA$$
	iota5f.3	$$⊢\left(\phi \wedge A\in V\right)\to \left(\psi \leftrightarrow x=A\right)$$
Assertion	iota5f	$$⊢\left(\phi \wedge A\in V\right)\to \left(\iota x|\psi \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		iota5f.1	$$⊢Ⅎx\phi$$
2		iota5f.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		iota5f.3	$$⊢\left(\phi \wedge A\in V\right)\to \left(\psi \leftrightarrow x=A\right)$$
4	2	nfel1	$$⊢ℲxA\in V$$
5	1 4	nfan	$$⊢Ⅎx\left(\phi \wedge A\in V\right)$$
6	5 3	alrimi	$$⊢\left(\phi \wedge A\in V\right)\to \forall x\left(\psi \leftrightarrow x=A\right)$$
7	2	nfeq2	$$⊢Ⅎxy=A$$
8		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
9	8	bibi2d	$$⊢y=A\to \left(\left(\psi \leftrightarrow x=y\right)\leftrightarrow \left(\psi \leftrightarrow x=A\right)\right)$$
10	7 9	albid	$$⊢y=A\to \left(\forall x\left(\psi \leftrightarrow x=y\right)\leftrightarrow \forall x\left(\psi \leftrightarrow x=A\right)\right)$$
11		eqeq2	$$⊢y=A\to \left(\left(\iota x|\psi \right)=y\leftrightarrow \left(\iota x|\psi \right)=A\right)$$
12	10 11	imbi12d	$$⊢y=A\to \left(\left(\forall x\left(\psi \leftrightarrow x=y\right)\to \left(\iota x|\psi \right)=y\right)\leftrightarrow \left(\forall x\left(\psi \leftrightarrow x=A\right)\to \left(\iota x|\psi \right)=A\right)\right)$$
13		iotaval	$$⊢\forall x\left(\psi \leftrightarrow x=y\right)\to \left(\iota x|\psi \right)=y$$
14	12 13	vtoclg	$$⊢A\in V\to \left(\forall x\left(\psi \leftrightarrow x=A\right)\to \left(\iota x|\psi \right)=A\right)$$
15	14	adantl	$$⊢\left(\phi \wedge A\in V\right)\to \left(\forall x\left(\psi \leftrightarrow x=A\right)\to \left(\iota x|\psi \right)=A\right)$$
16	6 15	mpd	$$⊢\left(\phi \wedge A\in V\right)\to \left(\iota x|\psi \right)=A$$