Metamath Proof Explorer

Theorem sbiota1

Description: Theorem *14.25 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 12-Jul-2011)

Ref Expression
Assertion sbiota1 
|- ( E! x ph -> ( A. x ( ph -> ps ) <-> [. ( iota x ph ) / x ]. ps ) )

Proof

Step Hyp Ref Expression
1 eu6 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
2 1 biimpi 
 |-  ( E! x ph -> E. y A. x ( ph <-> x = y ) )
3 iota4 
 |-  ( E! x ph -> [. ( iota x ph ) / x ]. ph )
4 iotaval 
 |-  ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
5 4 eqcomd 
 |-  ( A. x ( ph <-> x = y ) -> y = ( iota x ph ) )
6 spsbim 
 |-  ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
7 sbsbc 
 |-  ( [ y / x ] ph <-> [. y / x ]. ph )
8 sbsbc 
 |-  ( [ y / x ] ps <-> [. y / x ]. ps )
9 6 7 8 3imtr3g 
 |-  ( A. x ( ph -> ps ) -> ( [. y / x ]. ph -> [. y / x ]. ps ) )
10 dfsbcq 
 |-  ( y = ( iota x ph ) -> ( [. y / x ]. ph <-> [. ( iota x ph ) / x ]. ph ) )
11 dfsbcq 
 |-  ( y = ( iota x ph ) -> ( [. y / x ]. ps <-> [. ( iota x ph ) / x ]. ps ) )
12 10 11 imbi12d 
 |-  ( y = ( iota x ph ) -> ( ( [. y / x ]. ph -> [. y / x ]. ps ) <-> ( [. ( iota x ph ) / x ]. ph -> [. ( iota x ph ) / x ]. ps ) ) )
13 9 12 syl5ib 
 |-  ( y = ( iota x ph ) -> ( A. x ( ph -> ps ) -> ( [. ( iota x ph ) / x ]. ph -> [. ( iota x ph ) / x ]. ps ) ) )
14 13 com23 
 |-  ( y = ( iota x ph ) -> ( [. ( iota x ph ) / x ]. ph -> ( A. x ( ph -> ps ) -> [. ( iota x ph ) / x ]. ps ) ) )
15 5 14 syl 
 |-  ( A. x ( ph <-> x = y ) -> ( [. ( iota x ph ) / x ]. ph -> ( A. x ( ph -> ps ) -> [. ( iota x ph ) / x ]. ps ) ) )
16 15 exlimiv 
 |-  ( E. y A. x ( ph <-> x = y ) -> ( [. ( iota x ph ) / x ]. ph -> ( A. x ( ph -> ps ) -> [. ( iota x ph ) / x ]. ps ) ) )
17 2 3 16 sylc 
 |-  ( E! x ph -> ( A. x ( ph -> ps ) -> [. ( iota x ph ) / x ]. ps ) )
18 iotaexeu 
 |-  ( E! x ph -> ( iota x ph ) e. _V )
19 10 11 anbi12d 
 |-  ( y = ( iota x ph ) -> ( ( [. y / x ]. ph /\ [. y / x ]. ps ) <-> ( [. ( iota x ph ) / x ]. ph /\ [. ( iota x ph ) / x ]. ps ) ) )
20 19 imbi1d 
 |-  ( y = ( iota x ph ) -> ( ( ( [. y / x ]. ph /\ [. y / x ]. ps ) -> E. x ( ph /\ ps ) ) <-> ( ( [. ( iota x ph ) / x ]. ph /\ [. ( iota x ph ) / x ]. ps ) -> E. x ( ph /\ ps ) ) ) )
21 sbcan 
 |-  ( [. y / x ]. ( ph /\ ps ) <-> ( [. y / x ]. ph /\ [. y / x ]. ps ) )
22 spesbc 
 |-  ( [. y / x ]. ( ph /\ ps ) -> E. x ( ph /\ ps ) )
23 21 22 sylbir 
 |-  ( ( [. y / x ]. ph /\ [. y / x ]. ps ) -> E. x ( ph /\ ps ) )
24 20 23 vtoclg 
 |-  ( ( iota x ph ) e. _V -> ( ( [. ( iota x ph ) / x ]. ph /\ [. ( iota x ph ) / x ]. ps ) -> E. x ( ph /\ ps ) ) )
25 24 expd 
 |-  ( ( iota x ph ) e. _V -> ( [. ( iota x ph ) / x ]. ph -> ( [. ( iota x ph ) / x ]. ps -> E. x ( ph /\ ps ) ) ) )
26 18 3 25 sylc 
 |-  ( E! x ph -> ( [. ( iota x ph ) / x ]. ps -> E. x ( ph /\ ps ) ) )
27 26 anc2li 
 |-  ( E! x ph -> ( [. ( iota x ph ) / x ]. ps -> ( E! x ph /\ E. x ( ph /\ ps ) ) ) )
28 eupicka 
 |-  ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> A. x ( ph -> ps ) )
29 27 28 syl6 
 |-  ( E! x ph -> ( [. ( iota x ph ) / x ]. ps -> A. x ( ph -> ps ) ) )
30 17 29 impbid 
 |-  ( E! x ph -> ( A. x ( ph -> ps ) <-> [. ( iota x ph ) / x ]. ps ) )