Metamath Proof Explorer


Theorem hbsb

Description: If z is not free in ph , it is not free in [ y / x ] ph when y and z are distinct. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker hbsbw when possible. (Contributed by NM, 12-Aug-1993) (New usage is discouraged.)

Ref Expression
Hypothesis hbsb.1
|- ( ph -> A. z ph )
Assertion hbsb
|- ( [ y / x ] ph -> A. z [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 hbsb.1
 |-  ( ph -> A. z ph )
2 1 nf5i
 |-  F/ z ph
3 2 nfsb
 |-  F/ z [ y / x ] ph
4 3 nf5ri
 |-  ( [ y / x ] ph -> A. z [ y / x ] ph )