Theorem iota2df

Description: A condition that allows to represent "the unique element such that ph " with a class expression A . (Contributed by NM, 30-Dec-2014)

	Ref	Expression
Hypotheses	iota2df.1	$$⊢\phi \to B\in V$$
	iota2df.2	$$⊢\phi \to \exists !x\psi$$
	iota2df.3	$$⊢\left(\phi \wedge x=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
	iota2df.4	$$⊢Ⅎx\phi$$
	iota2df.5	$$⊢\phi \to Ⅎx\chi$$
	iota2df.6	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	iota2df	$$⊢\phi \to \left(\chi \leftrightarrow \left(\iota x|\psi \right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iota2df.1	$$⊢\phi \to B\in V$$
2		iota2df.2	$$⊢\phi \to \exists !x\psi$$
3		iota2df.3	$$⊢\left(\phi \wedge x=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		iota2df.4	$$⊢Ⅎx\phi$$
5		iota2df.5	$$⊢\phi \to Ⅎx\chi$$
6		iota2df.6	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
7		simpr	$$⊢\left(\phi \wedge x=B\right)\to x=B$$
8	7	eqeq2d	$$⊢\left(\phi \wedge x=B\right)\to \left(\left(\iota x|\psi \right)=x\leftrightarrow \left(\iota x|\psi \right)=B\right)$$
9	3 8	bibi12d	$$⊢\left(\phi \wedge x=B\right)\to \left(\left(\psi \leftrightarrow \left(\iota x|\psi \right)=x\right)\leftrightarrow \left(\chi \leftrightarrow \left(\iota x|\psi \right)=B\right)\right)$$
10		iota1	$$⊢\exists !x\psi \to \left(\psi \leftrightarrow \left(\iota x|\psi \right)=x\right)$$
11	2 10	syl	$$⊢\phi \to \left(\psi \leftrightarrow \left(\iota x|\psi \right)=x\right)$$
12		nfiota1	$$⊢\underset{\_}{Ⅎ}x\left(\iota x|\psi \right)$$
13	12	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\iota x|\psi \right)$$
14	13 6	nfeqd	$$⊢\phi \to Ⅎx\left(\iota x|\psi \right)=B$$
15	5 14	nfbid	$$⊢\phi \to Ⅎx\left(\chi \leftrightarrow \left(\iota x|\psi \right)=B\right)$$
16	1 9 11 4 6 15	vtocldf	$$⊢\phi \to \left(\chi \leftrightarrow \left(\iota x|\psi \right)=B\right)$$