Theorem iotasbc2

Description: Theorem *14.111 in WhiteheadRussell p. 184. (Contributed by Andrew Salmon, 11-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		iotasbc	|- ( E! x ph -> ( [. ( iota x ph ) / y ]. [. ( iota x ps ) / z ]. ch <-> E. y ( A. x ( ph <-> x = y ) /\ [. ( iota x ps ) / z ]. ch ) ) )
2		iotasbc	|- ( E! x ps -> ( [. ( iota x ps ) / z ]. ch <-> E. z ( A. x ( ps <-> x = z ) /\ ch ) ) )
3	2	anbi2d	|- ( E! x ps -> ( ( A. x ( ph <-> x = y ) /\ [. ( iota x ps ) / z ]. ch ) <-> ( A. x ( ph <-> x = y ) /\ E. z ( A. x ( ps <-> x = z ) /\ ch ) ) ) )
4		3anass	|- ( ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) <-> ( A. x ( ph <-> x = y ) /\ ( A. x ( ps <-> x = z ) /\ ch ) ) )
5	4	exbii	|- ( E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) <-> E. z ( A. x ( ph <-> x = y ) /\ ( A. x ( ps <-> x = z ) /\ ch ) ) )
6		19.42v	|- ( E. z ( A. x ( ph <-> x = y ) /\ ( A. x ( ps <-> x = z ) /\ ch ) ) <-> ( A. x ( ph <-> x = y ) /\ E. z ( A. x ( ps <-> x = z ) /\ ch ) ) )
7	5 6	bitr2i	|- ( ( A. x ( ph <-> x = y ) /\ E. z ( A. x ( ps <-> x = z ) /\ ch ) ) <-> E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) )
8	3 7	bitrdi	|- ( E! x ps -> ( ( A. x ( ph <-> x = y ) /\ [. ( iota x ps ) / z ]. ch ) <-> E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) ) )
9	8	exbidv	|- ( E! x ps -> ( E. y ( A. x ( ph <-> x = y ) /\ [. ( iota x ps ) / z ]. ch ) <-> E. y E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) ) )
10	1 9	sylan9bb	|- ( ( E! x ph /\ E! x ps ) -> ( [. ( iota x ph ) / y ]. [. ( iota x ps ) / z ]. ch <-> E. y E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) ) )