Theorem nfex 2358

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 2358, hbex 2359. (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 1813	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1890	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2357	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1886	1 ⊢ Ⅎ𝑥∃𝑦𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  hbex  2359  nfnf  2360  19.12  2361  eean  2381  eeeanv  2383  ee4anv  2384  moexexlem  2654  r19.12  3315  ceqsex2  3504  nfopab2  5182  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  axrep2  5241  axrep3  5242  copsex2t  5471  mosubopt  5489  mosubott  5491  euotd  5493  nfco  5854  dfdmf  5890  dfrnf  5944  nfdm  5945  fv3  6934  oprabv  7511  nfoprab2  7513  nfoprab3  7514  nfoprab  7515  cbvoprab1  7538  cbvoprab2  7539  cbvoprab3  7542  nffrecs  8339  ac6sfi  9313  aceq1  10235  zfcndrep  10738  zfcndinf  10742  nfsum1  15901  nfsum  15902  fsum2dlem  15980  nfcprod1  16121  nfcprod  16122  fprod2dlem  16191  brabgaf  33298  2ndresdju  33341  bnj981  35691  bnj1388  35774  bnj1445  35785  bnj1489  35797  fineqvrep  35923  bj-opabco  38377  pm11.71  45642  permaxrep  46260  upbdrech  46594  stoweidlem57  47340  or2expropbi  48377  ich2exprop  48826  ichnreuop  48827  ichreuopeq  48828  reuopreuprim  48881  pgind  51216  nfals  51327