Metamath Proof Explorer

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 
|- ( [ y / x ] E. x ph <-> E. x ph )

Proof

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