Theorem iotavalb

Description: Theorem *14.202 in WhiteheadRussell p. 189. A biconditional version of iotaval . (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotavalb	|- ( E! x ph -> ( A. x ( ph <-> x = y ) <-> ( iota x ph ) = y ) )

Proof

Step	Hyp	Ref	Expression
1		iotaval	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
2		iotasbc	|- ( E! x ph -> ( [. ( iota x ph ) / z ]. z = y <-> E. z ( A. x ( ph <-> x = z ) /\ z = y ) ) )
3		iotaexeu	|- ( E! x ph -> ( iota x ph ) e. _V )
4		eqsbc1	|- ( ( iota x ph ) e. _V -> ( [. ( iota x ph ) / z ]. z = y <-> ( iota x ph ) = y ) )
5	3 4	syl	|- ( E! x ph -> ( [. ( iota x ph ) / z ]. z = y <-> ( iota x ph ) = y ) )
6	2 5	bitr3d	|- ( E! x ph -> ( E. z ( A. x ( ph <-> x = z ) /\ z = y ) <-> ( iota x ph ) = y ) )
7		equequ2	|- ( z = y -> ( x = z <-> x = y ) )
8	7	bibi2d	|- ( z = y -> ( ( ph <-> x = z ) <-> ( ph <-> x = y ) ) )
9	8	albidv	|- ( z = y -> ( A. x ( ph <-> x = z ) <-> A. x ( ph <-> x = y ) ) )
10	9	biimpac	|- ( ( A. x ( ph <-> x = z ) /\ z = y ) -> A. x ( ph <-> x = y ) )
11	10	exlimiv	|- ( E. z ( A. x ( ph <-> x = z ) /\ z = y ) -> A. x ( ph <-> x = y ) )
12	6 11	syl6bir	|- ( E! x ph -> ( ( iota x ph ) = y -> A. x ( ph <-> x = y ) ) )
13	1 12	impbid2	|- ( E! x ph -> ( A. x ( ph <-> x = y ) <-> ( iota x ph ) = y ) )