Theorem iotavalsb

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

	Ref	Expression
Assertion	iotavalsb	|- ( A. x ( ph <-> x = y ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( A. x ( ph <-> x = y ) -> E. y A. x ( ph <-> x = y ) )
2		eu6	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
3		iotavalb	|- ( E! x ph -> ( A. x ( ph <-> x = y ) <-> ( iota x ph ) = y ) )
4		dfsbcq	|- ( y = ( iota x ph ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) )
5	4	eqcoms	|- ( ( iota x ph ) = y -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) )
6	3 5	syl6bi	|- ( E! x ph -> ( A. x ( ph <-> x = y ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) ) )
7	2 6	sylbir	|- ( E. y A. x ( ph <-> x = y ) -> ( A. x ( ph <-> x = y ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) ) )
8	1 7	mpcom	|- ( A. x ( ph <-> x = y ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) )