Theorem riotaxfrd

Description: Change the variable x in the expression for "the unique x such that ps " to another variable y contained in expression B . Use reuhypd to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riotaxfrd.1	|- F/_ y C
	riotaxfrd.2	|- ( ( ph /\ y e. A ) -> B e. A )
	riotaxfrd.3	|- ( ( ph /\ ( iota_ y e. A ch ) e. A ) -> C e. A )
	riotaxfrd.4	|- ( x = B -> ( ps <-> ch ) )
	riotaxfrd.5	|- ( y = ( iota_ y e. A ch ) -> B = C )
	riotaxfrd.6	|- ( ( ph /\ x e. A ) -> E! y e. A x = B )
Assertion	riotaxfrd	|- ( ( ph /\ E! x e. A ps ) -> ( iota_ x e. A ps ) = C )

Proof

Step	Hyp	Ref	Expression
1		riotaxfrd.1	|- F/_ y C
2		riotaxfrd.2	|- ( ( ph /\ y e. A ) -> B e. A )
3		riotaxfrd.3	|- ( ( ph /\ ( iota_ y e. A ch ) e. A ) -> C e. A )
4		riotaxfrd.4	|- ( x = B -> ( ps <-> ch ) )
5		riotaxfrd.5	|- ( y = ( iota_ y e. A ch ) -> B = C )
6		riotaxfrd.6	|- ( ( ph /\ x e. A ) -> E! y e. A x = B )
7		rabid	|- ( x e. { x e. A | ps } <-> ( x e. A /\ ps ) )
8	7	baib	|- ( x e. A -> ( x e. { x e. A | ps } <-> ps ) )
9	8	riotabiia	|- ( iota_ x e. A x e. { x e. A | ps } ) = ( iota_ x e. A ps )
10	2 6 4	reuxfr1ds	|- ( ph -> ( E! x e. A ps <-> E! y e. A ch ) )
11		riotacl2	|- ( E! y e. A ch -> ( iota_ y e. A ch ) e. { y e. A | ch } )
12	11	adantl	|- ( ( ph /\ E! y e. A ch ) -> ( iota_ y e. A ch ) e. { y e. A | ch } )
13		riotacl	|- ( E! y e. A ch -> ( iota_ y e. A ch ) e. A )
14		nfriota1	|- F/_ y ( iota_ y e. A ch )
15	14 1 2 4 5	rabxfrd	|- ( ( ph /\ ( iota_ y e. A ch ) e. A ) -> ( C e. { x e. A | ps } <-> ( iota_ y e. A ch ) e. { y e. A | ch } ) )
16	13 15	sylan2	|- ( ( ph /\ E! y e. A ch ) -> ( C e. { x e. A | ps } <-> ( iota_ y e. A ch ) e. { y e. A | ch } ) )
17	12 16	mpbird	|- ( ( ph /\ E! y e. A ch ) -> C e. { x e. A | ps } )
18	17	ex	|- ( ph -> ( E! y e. A ch -> C e. { x e. A | ps } ) )
19	10 18	sylbid	|- ( ph -> ( E! x e. A ps -> C e. { x e. A | ps } ) )
20	19	imp	|- ( ( ph /\ E! x e. A ps ) -> C e. { x e. A | ps } )
21	3	ex	|- ( ph -> ( ( iota_ y e. A ch ) e. A -> C e. A ) )
22	13 21	syl5	|- ( ph -> ( E! y e. A ch -> C e. A ) )
23	10 22	sylbid	|- ( ph -> ( E! x e. A ps -> C e. A ) )
24	23	imp	|- ( ( ph /\ E! x e. A ps ) -> C e. A )
25	7	baibr	|- ( x e. A -> ( ps <-> x e. { x e. A | ps } ) )
26	25	reubiia	|- ( E! x e. A ps <-> E! x e. A x e. { x e. A | ps } )
27	26	biimpi	|- ( E! x e. A ps -> E! x e. A x e. { x e. A | ps } )
28	27	adantl	|- ( ( ph /\ E! x e. A ps ) -> E! x e. A x e. { x e. A | ps } )
29		nfcv	|- F/_ x C
30		nfrab1	|- F/_ x { x e. A | ps }
31	30	nfel2	|- F/ x C e. { x e. A | ps }
32		eleq1	|- ( x = C -> ( x e. { x e. A | ps } <-> C e. { x e. A | ps } ) )
33	29 31 32	riota2f	|- ( ( C e. A /\ E! x e. A x e. { x e. A | ps } ) -> ( C e. { x e. A | ps } <-> ( iota_ x e. A x e. { x e. A | ps } ) = C ) )
34	24 28 33	syl2anc	|- ( ( ph /\ E! x e. A ps ) -> ( C e. { x e. A | ps } <-> ( iota_ x e. A x e. { x e. A | ps } ) = C ) )
35	20 34	mpbid	|- ( ( ph /\ E! x e. A ps ) -> ( iota_ x e. A x e. { x e. A | ps } ) = C )
36	9 35	eqtr3id	|- ( ( ph /\ E! x e. A ps ) -> ( iota_ x e. A ps ) = C )