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 1782	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1859	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2328	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1859	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1855	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  hbex  2330  nfnf  2331  19.12  2332  eean  2352  eeeanv  2354  ee4anv  2355  moexexlem  2626  r19.12  3286  ceqsex2  3481  nfopab2  5156  cbvopab1  5159  cbvopab1g  5160  cbvopab1s  5162  axrep2  5215  axrep3  5216  axrep4OLD  5219  copsex2t  5446  mosubopt  5464  euotd  5467  nfco  5820  dfdmf  5851  dfrnf  5905  nfdm  5906  fv3  6858  oprabv  7427  nfoprab2  7429  nfoprab3  7430  nfoprab  7431  cbvoprab1  7454  cbvoprab2  7455  cbvoprab3  7458  nffrecs  8233  ac6sfi  9194  aceq1  10039  zfcndrep  10537  zfcndinf  10541  nfsum1  15652  nfsum  15653  fsum2dlem  15732  nfcprod1  15873  nfcprod  15874  fprod2dlem  15945  brabgaf  32679  2ndresdju  32722  bnj981  35092  bnj1388  35175  bnj1445  35186  bnj1489  35198  fineqvrep  35258  bj-opabco  37502  pm11.71  44824  permaxrep  45433  upbdrech  45738  stoweidlem57  46485  or2expropbi  47482  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  reuopreuprim  47986  pgind  50192