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

Metamath Proof Explorer

Theorem nfe1

Description: The setvar x is not free in E. x ph . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion nfe1 Ⅎ 𝑥 ∃ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 hbe1 ⊢ ( ∃ 𝑥 𝜑 → ∀ 𝑥 ∃ 𝑥 𝜑 )
2 1 nf5i ⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑