Metamath Proof Explorer

Theorem bj-sbf4

Description: Substitution has no effect on a bound variable (nonfreeness case); see sbf2 . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-sbf4 
|- ( [ y / x ] F/ x ph <-> F/ x ph )

Proof

Step Hyp Ref Expression
1 nfnf1 
 |-  F/ x F/ x ph
2 1 sbf 
 |-  ( [ y / x ] F/ x ph <-> F/ x ph )