Theorem nfexd 2363

Description: If 𝑥 is not free in 𝜓, then it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
nfald.1	⊢ Ⅎ𝑦𝜑
nfald.2	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfexd	⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)

Proof of Theorem nfexd

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfmod2  2586  nfmodv  2587  nfeudw  2619  nfeld  2937  nfopabd  5176  nfttrcld  9735  axrepndlem1  10701  axrepndlem2  10702  axunndlem1  10704  axunnd  10705  axpowndlem2  10707  axpowndlem3  10708  axpowndlem4  10709  axregndlem2  10712  axinfndlem1  10714  axinfnd  10715  axacndlem4  10719  axacndlem5  10720  axacnd  10721  19.9d2rf  33135  axsepg2  35907  axpowg2  35914  axpowg3  35915  hbexg  45728