Theorem nfexd 2323

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfmod2  2558  nfmodv  2559  nfeudw  2591  nfeld  2918  nfopabd  5142  nfttrcld  9468  axrepndlem1  10348  axrepndlem2  10349  axunndlem1  10351  axunnd  10352  axpowndlem2  10354  axpowndlem3  10355  axpowndlem4  10356  axregndlem2  10359  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  19.9d2rf  30820  hbexg  42176