Theorem iota5

Description: A method for computing iota. (Contributed by NM, 17-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		iota5.1	$$⊢\left(\phi \wedge A\in V\right)\to \left(\psi \leftrightarrow x=A\right)$$
2	1	alrimiv	$$⊢\left(\phi \wedge A\in V\right)\to \forall x\left(\psi \leftrightarrow x=A\right)$$
3		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
4	3	bibi2d	$$⊢y=A\to \left(\left(\psi \leftrightarrow x=y\right)\leftrightarrow \left(\psi \leftrightarrow x=A\right)\right)$$
5	4	albidv	$$⊢y=A\to \left(\forall x\left(\psi \leftrightarrow x=y\right)\leftrightarrow \forall x\left(\psi \leftrightarrow x=A\right)\right)$$
6		eqeq2	$$⊢y=A\to \left(\left(\iota x|\psi \right)=y\leftrightarrow \left(\iota x|\psi \right)=A\right)$$
7	5 6	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)$$
8		iotaval	$$⊢\forall x\left(\psi \leftrightarrow x=y\right)\to \left(\iota x|\psi \right)=y$$
9	7 8	vtoclg	$$⊢A\in V\to \left(\forall x\left(\psi \leftrightarrow x=A\right)\to \left(\iota x|\psi \right)=A\right)$$
10	9	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)$$
11	2 10	mpd	$$⊢\left(\phi \wedge A\in V\right)\to \left(\iota x|\psi \right)=A$$