Theorem nfex 2359

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 2359, hbex 2360. (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 2358	. . 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 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195  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  2360  nfnf  2361  19.12  2362  eean  2382  eeeanv  2384  ee4anv  2385  moexexlem  2656  r19.12  3316  ceqsex2  3507  nfopab2  5184  cbvopab1  5187  cbvopab1g  5188  cbvopab1s  5190  axrep2  5243  axrep3  5244  axrep4OLD  5247  copsex2t  5477  mosubopt  5495  euotd  5498  nfco  5853  dfdmf  5888  dfrnf  5942  nfdm  5943  fv3  6903  oprabv  7479  nfoprab2  7481  nfoprab3  7482  nfoprab  7483  cbvoprab1  7506  cbvoprab2  7507  cbvoprab3  7510  nffrecs  8286  ac6sfi  9251  aceq1  10117  zfcndrep  10616  zfcndinf  10620  nfsum1  15767  nfsum  15768  fsum2dlem  15846  nfcprod1  15987  nfcprod  15988  fprod2dlem  16059  brabgaf  33024  2ndresdju  33067  bnj981  35405  bnj1388  35488  bnj1445  35499  bnj1489  35511  fineqvrep  35586  bj-opabco  37891  pm11.71  45167  permaxrep  45775  upbdrech  46084  stoweidlem57  46831  or2expropbi  47831  ich2exprop  48280  ichnreuop  48281  ichreuopeq  48282  reuopreuprim  48335  pgind  50554  nfals  50640