Metamath Proof Explorer

Theorem iotasbcq

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

Ref Expression
Assertion iotasbcq 
|- ( A. x ( ph <-> ps ) -> ( [. ( iota x ph ) / y ]. ch <-> [. ( iota x ps ) / y ]. ch ) )

Proof

Step Hyp Ref Expression
1 iotabi 
 |-  ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )
2 1 sbceq1d 
 |-  ( A. x ( ph <-> ps ) -> ( [. ( iota x ph ) / y ]. ch <-> [. ( iota x ps ) / y ]. ch ) )