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

Metamath Proof Explorer

Theorem nfi

Description: Deduce that x is not free in ph from the definition. (Contributed by Wolf Lammen, 15-Sep-2021)

Ref Expression
Hypothesis nfi.1 ⊢ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 )
Assertion nfi Ⅎ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 nfi.1 ⊢ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 )
2 df-nf ⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
3 1 2 mpbir ⊢ Ⅎ 𝑥 𝜑