Metamath Proof Explorer

Theorem sbf2

Description: Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005)

Ref Expression
Assertion sbf2 
|- ( [ y / x ] A. x ph <-> A. x ph )

Proof

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