Metamath Proof Explorer

Theorem riotasvd

Description: Deduction version of riotasv . (Contributed by NM, 4-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riotasvd.1 
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
riotasvd.2 
|- ( ph -> D e. A )
Assertion riotasvd 
|- ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) )

Proof

Step Hyp Ref Expression
1 riotasvd.1 
 |-  ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
2 riotasvd.2 
 |-  ( ph -> D e. A )
3 1 adantr 
 |-  ( ( ph /\ A e. V ) -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )
4 2 adantr 
 |-  ( ( ph /\ A e. V ) -> D e. A )
5 3 4 eqeltrrd 
 |-  ( ( ph /\ A e. V ) -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) e. A )
6 riotaclbgBAD 
 |-  ( A e. V -> ( E! x e. A A. y e. B ( ps -> x = C ) <-> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) e. A ) )
7 6 adantl 
 |-  ( ( ph /\ A e. V ) -> ( E! x e. A A. y e. B ( ps -> x = C ) <-> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) e. A ) )
8 5 7 mpbird 
 |-  ( ( ph /\ A e. V ) -> E! x e. A A. y e. B ( ps -> x = C ) )
9 riotasbc 
 |-  ( E! x e. A A. y e. B ( ps -> x = C ) -> [. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) / x ]. A. y e. B ( ps -> x = C ) )
10 8 9 syl 
 |-  ( ( ph /\ A e. V ) -> [. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) / x ]. A. y e. B ( ps -> x = C ) )
11 eqeq1 
 |-  ( x = z -> ( x = C <-> z = C ) )
12 11 imbi2d 
 |-  ( x = z -> ( ( ps -> x = C ) <-> ( ps -> z = C ) ) )
13 12 ralbidv 
 |-  ( x = z -> ( A. y e. B ( ps -> x = C ) <-> A. y e. B ( ps -> z = C ) ) )
14 nfra1 
 |-  F/ y A. y e. B ( ps -> x = C )
15 nfcv 
 |-  F/_ y A
16 14 15 nfriota 
 |-  F/_ y ( iota_ x e. A A. y e. B ( ps -> x = C ) )
17 16 nfeq2 
 |-  F/ y z = ( iota_ x e. A A. y e. B ( ps -> x = C ) )
18 eqeq1 
 |-  ( z = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) -> ( z = C <-> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) )
19 18 imbi2d 
 |-  ( z = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) -> ( ( ps -> z = C ) <-> ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
20 17 19 ralbid 
 |-  ( z = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) -> ( A. y e. B ( ps -> z = C ) <-> A. y e. B ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
21 13 20 sbcie2g 
 |-  ( ( iota_ x e. A A. y e. B ( ps -> x = C ) ) e. A -> ( [. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) / x ]. A. y e. B ( ps -> x = C ) <-> A. y e. B ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
22 5 21 syl 
 |-  ( ( ph /\ A e. V ) -> ( [. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) / x ]. A. y e. B ( ps -> x = C ) <-> A. y e. B ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
23 10 22 mpbid 
 |-  ( ( ph /\ A e. V ) -> A. y e. B ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) )
24 rsp 
 |-  ( A. y e. B ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) -> ( y e. B -> ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
25 23 24 syl 
 |-  ( ( ph /\ A e. V ) -> ( y e. B -> ( ps -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) ) )
26 25 impd 
 |-  ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) )
27 3 eqeq1d 
 |-  ( ( ph /\ A e. V ) -> ( D = C <-> ( iota_ x e. A A. y e. B ( ps -> x = C ) ) = C ) )
28 26 27 sylibrd 
 |-  ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) )