Metamath Proof Explorer

Theorem nfe2

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

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

Proof

Step Hyp Ref Expression
1 excom 
 |-  ( E. y E. x ph <-> E. x E. y ph )
2 nfe1 
 |-  F/ x E. x E. y ph
3 1 2 nfxfr 
 |-  F/ x E. y E. x ph