Metamath Proof Explorer

Theorem nfexa2

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

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

Proof

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