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 ) ) )