Theorem bj-sbf3

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

	Ref	Expression
Assertion	bj-sbf3	$$⊢\left[y/x\right]\exists x\phi \leftrightarrow \exists x\phi$$

Proof

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