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

Metamath Proof Explorer

Theorem iotasbc

Description: Definition *14.01 in WhiteheadRussell p. 184. In Principia Mathematica, Russell and Whitehead define iota in terms of a function of ( iota x ph ) . Their definition differs in that a function of ( iota x ph ) evaluates to "false" when there isn't a single x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 sbc5 
 |-  ( [. ( iota x ph ) / y ]. ps <-> E. y ( y = ( iota x ph ) /\ ps ) )
2 iotaexeu 
 |-  ( E! x ph -> ( iota x ph ) e. _V )
3 eueq 
 |-  ( ( iota x ph ) e. _V <-> E! y y = ( iota x ph ) )
4 2 3 sylib 
 |-  ( E! x ph -> E! y y = ( iota x ph ) )
5 eu6 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
6 iotaval 
 |-  ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
7 6 eqcomd 
 |-  ( A. x ( ph <-> x = y ) -> y = ( iota x ph ) )
8 7 ancri 
 |-  ( A. x ( ph <-> x = y ) -> ( y = ( iota x ph ) /\ A. x ( ph <-> x = y ) ) )
9 8 eximi 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. y ( y = ( iota x ph ) /\ A. x ( ph <-> x = y ) ) )
10 5 9 sylbi 
 |-  ( E! x ph -> E. y ( y = ( iota x ph ) /\ A. x ( ph <-> x = y ) ) )
11 eupick 
 |-  ( ( E! y y = ( iota x ph ) /\ E. y ( y = ( iota x ph ) /\ A. x ( ph <-> x = y ) ) ) -> ( y = ( iota x ph ) -> A. x ( ph <-> x = y ) ) )
12 4 10 11 syl2anc 
 |-  ( E! x ph -> ( y = ( iota x ph ) -> A. x ( ph <-> x = y ) ) )
13 12 7 impbid1 
 |-  ( E! x ph -> ( y = ( iota x ph ) <-> A. x ( ph <-> x = y ) ) )
14 13 anbi1d 
 |-  ( E! x ph -> ( ( y = ( iota x ph ) /\ ps ) <-> ( A. x ( ph <-> x = y ) /\ ps ) ) )
15 14 exbidv 
 |-  ( E! x ph -> ( E. y ( y = ( iota x ph ) /\ ps ) <-> E. y ( A. x ( ph <-> x = y ) /\ ps ) ) )
16 1 15 bitrid 
 |-  ( E! x ph -> ( [. ( iota x ph ) / y ]. ps <-> E. y ( A. x ( ph <-> x = y ) /\ ps ) ) )