Theorem riota2f

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

	Ref	Expression
Hypotheses	riota2f.1	$$⊢\underset{\_}{Ⅎ}xB$$
	riota2f.2	$$⊢Ⅎx\psi$$
	riota2f.3	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		riota2f.1	$$⊢\underset{\_}{Ⅎ}xB$$
2		riota2f.2	$$⊢Ⅎx\psi$$
3		riota2f.3	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
4	1	nfel1	$$⊢ℲxB\in A$$
5	1	a1i	$$⊢B\in A\to \underset{\_}{Ⅎ}xB$$
6	2	a1i	$$⊢B\in A\to Ⅎx\psi$$
7		id	$$⊢B\in A\to B\in A$$
8	3	adantl	$$⊢\left(B\in A\wedge x=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
9	4 5 6 7 8	riota2df	$$⊢\left(B\in A\wedge \exists !x\in A\phi \right)\to \left(\psi \leftrightarrow \left(\iota x\in A|\phi \right)=B\right)$$