Theorem nfex 2330

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 2330, hbex 2331. (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 2329	. . 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  2331  nfnf  2332  19.12  2333  eean  2353  eeeanv  2355  ee4anv  2356  moexexlem  2627  r19.12  3287  ceqsex2  3482  nfopab2  5157  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  axrep2  5216  axrep3  5217  axrep4OLD  5220  copsex2t  5441  mosubopt  5459  euotd  5462  nfco  5815  dfdmf  5846  dfrnf  5900  nfdm  5901  fv3  6853  oprabv  7421  nfoprab2  7423  nfoprab3  7424  nfoprab  7425  cbvoprab1  7448  cbvoprab2  7449  cbvoprab3  7452  nffrecs  8227  ac6sfi  9188  aceq1  10033  zfcndrep  10531  zfcndinf  10535  nfsum1  15646  nfsum  15647  fsum2dlem  15726  nfcprod1  15867  nfcprod  15868  fprod2dlem  15939  brabgaf  32697  2ndresdju  32740  bnj981  35111  bnj1388  35194  bnj1445  35205  bnj1489  35217  fineqvrep  35277  bj-opabco  37521  pm11.71  44845  permaxrep  45454  upbdrech  45759  stoweidlem57  46506  or2expropbi  47497  ich2exprop  47946  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  pgind  50207