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

Metamath Proof Explorer

Theorem nfexd

Description: If x is not free in ps , then it is not free in E. y ps . (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypotheses nfald.1 ⊢ Ⅎ 𝑦 𝜑
nfald.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion nfexd ( 𝜑 → Ⅎ 𝑥 ∃ 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 nfald.1 ⊢ Ⅎ 𝑦 𝜑
2 nfald.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 df-ex ⊢ ( ∃ 𝑦 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜓 )
4 2 nfnd ⊢ ( 𝜑 → Ⅎ 𝑥 ¬ 𝜓 )
5 1 4 nfald ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ¬ 𝜓 )
6 5 nfnd ⊢ ( 𝜑 → Ⅎ 𝑥 ¬ ∀ 𝑦 ¬ 𝜓 )
7 3 6 nfxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑦 𝜓 )