Theorem riotaprop

Description: Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013)

	Ref	Expression
Hypotheses	riotaprop.0	$$⊢Ⅎx\psi$$
	riotaprop.1	$$⊢B=\left(\iota x\in A|\phi \right)$$
	riotaprop.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	riotaprop	$$⊢\exists !x\in A\phi \to \left(B\in A\wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaprop.0	$$⊢Ⅎx\psi$$
2		riotaprop.1	$$⊢B=\left(\iota x\in A|\phi \right)$$
3		riotaprop.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
4		riotacl	$$⊢\exists !x\in A\phi \to \left(\iota x\in A|\phi \right)\in A$$
5	2 4	eqeltrid	$$⊢\exists !x\in A\phi \to B\in A$$
6	2	eqcomi	$$⊢\left(\iota x\in A|\phi \right)=B$$
7		nfriota1	$$⊢\underset{\_}{Ⅎ}x\left(\iota x\in A|\phi \right)$$
8	2 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}xB$$
9	8 1 3	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)$$
10	6 9	mpbiri	$$⊢\left(B\in A\wedge \exists !x\in A\phi \right)\to \psi$$
11	5 10	mpancom	$$⊢\exists !x\in A\phi \to \psi$$
12	5 11	jca	$$⊢\exists !x\in A\phi \to \left(B\in A\wedge \psi \right)$$