Metamath Proof Explorer

Theorem riotass2

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)

Ref Expression
Assertion riotass2 
|- ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ps ) )

Proof

Step Hyp Ref Expression
1 reuss2 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> E! x e. A ph )
2 simplr 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> A. x e. A ( ph -> ps ) )
3 riotasbc 
 |-  ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )
4 riotacl 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
5 rspsbc 
 |-  ( ( iota_ x e. A ph ) e. A -> ( A. x e. A ( ph -> ps ) -> [. ( iota_ x e. A ph ) / x ]. ( ph -> ps ) ) )
6 sbcimg 
 |-  ( ( iota_ x e. A ph ) e. A -> ( [. ( iota_ x e. A ph ) / x ]. ( ph -> ps ) <-> ( [. ( iota_ x e. A ph ) / x ]. ph -> [. ( iota_ x e. A ph ) / x ]. ps ) ) )
7 5 6 sylibd 
 |-  ( ( iota_ x e. A ph ) e. A -> ( A. x e. A ( ph -> ps ) -> ( [. ( iota_ x e. A ph ) / x ]. ph -> [. ( iota_ x e. A ph ) / x ]. ps ) ) )
8 4 7 syl 
 |-  ( E! x e. A ph -> ( A. x e. A ( ph -> ps ) -> ( [. ( iota_ x e. A ph ) / x ]. ph -> [. ( iota_ x e. A ph ) / x ]. ps ) ) )
9 3 8 mpid 
 |-  ( E! x e. A ph -> ( A. x e. A ( ph -> ps ) -> [. ( iota_ x e. A ph ) / x ]. ps ) )
10 1 2 9 sylc 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> [. ( iota_ x e. A ph ) / x ]. ps )
11 1 4 syl 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) e. A )
12 ssel 
 |-  ( A C_ B -> ( ( iota_ x e. A ph ) e. A -> ( iota_ x e. A ph ) e. B ) )
13 12 ad2antrr 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( ( iota_ x e. A ph ) e. A -> ( iota_ x e. A ph ) e. B ) )
14 11 13 mpd 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) e. B )
15 simprr 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> E! x e. B ps )
16 nfriota1 
 |-  F/_ x ( iota_ x e. A ph )
17 16 nfsbc1 
 |-  F/ x [. ( iota_ x e. A ph ) / x ]. ps
18 sbceq1a 
 |-  ( x = ( iota_ x e. A ph ) -> ( ps <-> [. ( iota_ x e. A ph ) / x ]. ps ) )
19 16 17 18 riota2f 
 |-  ( ( ( iota_ x e. A ph ) e. B /\ E! x e. B ps ) -> ( [. ( iota_ x e. A ph ) / x ]. ps <-> ( iota_ x e. B ps ) = ( iota_ x e. A ph ) ) )
20 14 15 19 syl2anc 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( [. ( iota_ x e. A ph ) / x ]. ps <-> ( iota_ x e. B ps ) = ( iota_ x e. A ph ) ) )
21 10 20 mpbid 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. B ps ) = ( iota_ x e. A ph ) )
22 21 eqcomd 
 |-  ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ps ) )