Theorem nfex 2333

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 2333, hbex 2334. (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 1787	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1864	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2332	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1864	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1860	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1545  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  hbex  2334  nfnf  2335  19.12  2336  eean  2356  eeeanv  2358  ee4anv  2359  moexexlem  2630  r19.12  3288  ceqsex2  3482  nfopab2  5143  cbvopab1  5146  cbvopab1g  5147  cbvopab1s  5149  axrep2  5202  axrep3  5203  axrep4OLD  5206  copsex2t  5433  mosubopt  5451  euotd  5454  nfco  5807  dfdmf  5838  dfrnf  5892  nfdm  5893  fv3  6845  oprabv  7416  nfoprab2  7418  nfoprab3  7419  nfoprab  7420  cbvoprab1  7443  cbvoprab2  7444  cbvoprab3  7447  nffrecs  8223  ac6sfi  9184  aceq1  10030  zfcndrep  10528  zfcndinf  10532  nfsum1  15643  nfsum  15644  fsum2dlem  15723  nfcprod1  15864  nfcprod  15865  fprod2dlem  15936  brabgaf  32698  2ndresdju  32741  bnj981  35132  bnj1388  35215  bnj1445  35226  bnj1489  35238  fineqvrep  35295  bj-opabco  37548  pm11.71  44841  permaxrep  45450  upbdrech  45753  stoweidlem57  46500  or2expropbi  47497  ich2exprop  47946  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  pgind  50207