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

Metamath Proof Explorer

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