Theorem nfex 2355

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 2355, hbex 2356. (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 2354	. . 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 2178  ax-11 2194  ax-12 2213

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

This theorem is used by:  hbex  2356  nfnf  2357  19.12  2358  eean  2378  eeeanv  2380  ee4anv  2381  moexexlem  2652  r19.12  3312  ceqsex2  3501  nfopab2  5176  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  axrep2  5235  axrep3  5236  copsex2t  5464  mosubopt  5482  mosubott  5484  euotd  5486  nfco  5843  dfdmf  5878  dfrnf  5932  nfdm  5933  fv3  6903  oprabv  7480  nfoprab2  7482  nfoprab3  7483  nfoprab  7484  cbvoprab1  7507  cbvoprab2  7508  cbvoprab3  7511  nffrecs  8301  ac6sfi  9275  aceq1  10196  zfcndrep  10699  zfcndinf  10703  nfsum1  15857  nfsum  15858  fsum2dlem  15936  nfcprod1  16077  nfcprod  16078  fprod2dlem  16147  brabgaf  33200  2ndresdju  33243  bnj981  35580  bnj1388  35663  bnj1445  35674  bnj1489  35686  fineqvrep  35782  bj-opabco  38109  pm11.71  45380  permaxrep  45995  upbdrech  46320  stoweidlem57  47066  or2expropbi  48103  ich2exprop  48552  ichnreuop  48553  ichreuopeq  48554  reuopreuprim  48607  pgind  50809  nfals  50898