Theorem iota2d

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)$$
Assertion	iota2d	$$⊢\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		nfv	$$⊢Ⅎx\phi$$
5		nfvd	$$⊢\phi \to Ⅎx\chi$$
6		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
7	1 2 3 4 5 6	iota2df	$$⊢\phi \to \left(\chi \leftrightarrow \left(\iota x|\psi \right)=B\right)$$