Metamath Proof Explorer

Theorem nfale2

Description: An inner existential quantifier's variable is bound. (Contributed by SN, 11-Feb-2026)

Ref Expression
Assertion nfale2 
|- F/ x A. y E. x ph

Proof

Step Hyp Ref Expression
1 hbe1 
 |-  ( E. x ph -> A. x E. x ph )
2 1 nfalh 
 |-  F/ x A. y E. x ph