Theorem nfex 2329

Description: If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2329, hbex 2330. (Revised by Wolf Lammen, 16-Oct-2021.)

Hypothesis

Ref	Expression
nfex.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfex	⊢ Ⅎ𝑥∃𝑦𝜑

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		df-ex 1781	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1858	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2328	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  hbex  2330  nfnf  2331  19.12  2332  eean  2352  eeeanv  2354  ee4anv  2355  moexexlem  2626  r19.12  3285  ceqsex2  3493  nfopab2  5169  cbvopab1  5172  cbvopab1g  5173  cbvopab1s  5175  axrep2  5227  axrep3  5228  axrep4OLD  5231  copsex2t  5440  mosubopt  5458  euotd  5461  nfco  5814  dfdmf  5845  dfrnf  5899  nfdm  5900  fv3  6852  oprabv  7418  nfoprab2  7420  nfoprab3  7421  nfoprab  7422  cbvoprab1  7445  cbvoprab2  7446  cbvoprab3  7449  nffrecs  8225  ac6sfi  9184  aceq1  10027  zfcndrep  10525  zfcndinf  10529  nfsum1  15613  nfsum  15614  fsum2dlem  15693  nfcprod1  15831  nfcprod  15832  fprod2dlem  15903  brabgaf  32684  2ndresdju  32727  bnj981  35106  bnj1388  35189  bnj1445  35200  bnj1489  35212  fineqvrep  35270  bj-opabco  37393  pm11.71  44648  permaxrep  45257  upbdrech  45563  stoweidlem57  46311  or2expropbi  47290  ich2exprop  47727  ichnreuop  47728  ichreuopeq  47729  reuopreuprim  47782  pgind  49972