Metamath Proof Explorer

Theorem riotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 reuss 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. A ph )
2 riotasbc 
 |-  ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )
3 1 2 syl 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> [. ( iota_ x e. A ph ) / x ]. ph )
4 simp1 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> A C_ B )
5 riotacl 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
6 1 5 syl 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) e. A )
7 4 6 sseldd 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) e. B )
8 simp3 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. B ph )
9 nfriota1 
 |-  F/_ x ( iota_ x e. A ph )
10 9 nfsbc1 
 |-  F/ x [. ( iota_ x e. A ph ) / x ]. ph
11 sbceq1a 
 |-  ( x = ( iota_ x e. A ph ) -> ( ph <-> [. ( iota_ x e. A ph ) / x ]. ph ) )
12 9 10 11 riota2f 
 |-  ( ( ( iota_ x e. A ph ) e. B /\ E! x e. B ph ) -> ( [. ( iota_ x e. A ph ) / x ]. ph <-> ( iota_ x e. B ph ) = ( iota_ x e. A ph ) ) )
13 7 8 12 syl2anc 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( [. ( iota_ x e. A ph ) / x ]. ph <-> ( iota_ x e. B ph ) = ( iota_ x e. A ph ) ) )
14 3 13 mpbid 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. B ph ) = ( iota_ x e. A ph ) )
15 14 eqcomd 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )