Theorem riotaprop

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

	Ref	Expression
Hypotheses	riotaprop.0	|- F/ x ps
	riotaprop.1	|- B = ( iota_ x e. A ph )
	riotaprop.2	|- ( x = B -> ( ph <-> ps ) )
Assertion	riotaprop	|- ( E! x e. A ph -> ( B e. A /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		riotaprop.0	|- F/ x ps
2		riotaprop.1	|- B = ( iota_ x e. A ph )
3		riotaprop.2	|- ( x = B -> ( ph <-> ps ) )
4		riotacl	|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
5	2 4	eqeltrid	|- ( E! x e. A ph -> B e. A )
6	2	eqcomi	|- ( iota_ x e. A ph ) = B
7		nfriota1	|- F/_ x ( iota_ x e. A ph )
8	2 7	nfcxfr	|- F/_ x B
9	8 1 3	riota2f	|- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
10	6 9	mpbiri	|- ( ( B e. A /\ E! x e. A ph ) -> ps )
11	5 10	mpancom	|- ( E! x e. A ph -> ps )
12	5 11	jca	|- ( E! x e. A ph -> ( B e. A /\ ps ) )