Theorem riota2

Description: This theorem shows a condition that allows us to represent a descriptor with a class expression B . (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 10-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		riota2.1	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
3		nfv	$$⊢Ⅎx\psi$$
4	2 3 1	riota2f	$$⊢\left(B\in A\wedge \exists !x\in A\phi \right)\to \left(\psi \leftrightarrow \left(\iota x\in A|\phi \right)=B\right)$$