This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfe2

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

Ref Expression
Assertion nfe2 Ⅎ 𝑥 ∃ 𝑦 ∃ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
2 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∃ 𝑦 𝜑
3 1 2 nfxfr ⊢ Ⅎ 𝑥 ∃ 𝑦 ∃ 𝑥 𝜑