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

Metamath Proof Explorer

Theorem nfexa2

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

Ref Expression
Assertion nfexa2 Ⅎ 𝑥 ∃ 𝑦 ∀ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 hbe1a ⊢ ( ∃ 𝑥 ∀ 𝑥 𝜑 → ∀ 𝑥 𝜑 )
2 1 nfexhe ⊢ Ⅎ 𝑥 ∃ 𝑦 ∀ 𝑥 𝜑