Theorem nfexd 2328

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 1780	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2		nfald.1	. . . 4 ⊢ Ⅎ𝑦𝜑
3		nfald.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	3	nfnd 1858	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
5	2, 4	nfald 2327	. . 3 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ¬ 𝜓)
6	5	nfnd 1858	. 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
7	1, 6	nfxfrd 1854	1 ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfmod2  2552  nfmodv  2553  nfeudw  2585  nfeld  2904  nfopabd  5178  nfttrcld  9670  axrepndlem1  10552  axrepndlem2  10553  axunndlem1  10555  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  19.9d2rf  32405  hbexg  44553