Metamath Proof Explorer

Theorem sbeqi

Description: Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018)

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

Proof

Step Hyp Ref Expression
1 spsbbi 
 |-  ( A. z ( ph <-> ps ) -> ( [ x / z ] ph <-> [ x / z ] ps ) )
2 sbequ 
 |-  ( x = y -> ( [ x / z ] ps <-> [ y / z ] ps ) )
3 1 2 sylan9bbr 
 |-  ( ( x = y /\ A. z ( ph <-> ps ) ) -> ( [ x / z ] ph <-> [ y / z ] ps ) )