This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )