Theorem sbf2

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

	Ref	Expression
Assertion	sbf2	$$⊢\left[y/x\right]\forall x\phi \leftrightarrow \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall x\phi$$
2	1	sbf	$$⊢\left[y/x\right]\forall x\phi \leftrightarrow \forall x\phi$$