Theorem nfexd 2355

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1552  ∃wex 1793  Ⅎwnf 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-10 2169  ax-11 2185  ax-12 2206

This theorem depends on definitions:  df-bi 209  df-or 857  df-ex 1794  df-nf 1798

This theorem is referenced by:  nfmod2  2579  nfmodv  2580  nfeudw  2612  nfeld  2929  nfopabd  5162  nfttrcld  9655  axrepndlem1  10540  axrepndlem2  10541  axunndlem1  10543  axunnd  10544  axpowndlem2  10546  axpowndlem3  10547  axpowndlem4  10548  axregndlem2  10551  axinfndlem1  10553  axinfnd  10554  axacndlem4  10558  axacndlem5  10559  axacnd  10560  19.9d2rf  32609  axsepg2  35391  axpowg2  35398  axpowg3  35399  hbexg  45080