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  2551  nfmodv  2552  nfeudw  2584  nfeld  2903  nfopabd  5175  nfttrcld  9663  axrepndlem1  10545  axrepndlem2  10546  axunndlem1  10548  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axregndlem2  10556  axinfndlem1  10558  axinfnd  10559  axacndlem4  10563  axacndlem5  10564  axacnd  10565  19.9d2rf  32398  hbexg  44546