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 x φ x φ

Proof

Step Hyp Ref Expression
1 nfnf1 x x φ
2 1 sbf y x x φ x φ