Theorem nfex 2354

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 2354, hbex 2355. (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 2353	. . 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  2355  nfnf  2356  19.12  2357  eean  2377  eeeanv  2379  ee4anv  2380  moexexlem  2651  r19.12  3311  ceqsex2  3500  nfopab2  5176  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  axrep2  5235  axrep3  5236  axrep4OLD  5239  copsex2t  5469  mosubopt  5487  euotd  5490  nfco  5845  dfdmf  5880  dfrnf  5934  nfdm  5935  fv3  6897  oprabv  7474  nfoprab2  7476  nfoprab3  7477  nfoprab  7478  cbvoprab1  7501  cbvoprab2  7502  cbvoprab3  7505  nffrecs  8283  ac6sfi  9255  aceq1  10121  zfcndrep  10624  zfcndinf  10628  nfsum1  15778  nfsum  15779  fsum2dlem  15857  nfcprod1  15998  nfcprod  15999  fprod2dlem  16068  brabgaf  33080  2ndresdju  33123  bnj981  35460  bnj1388  35543  bnj1445  35554  bnj1489  35566  fineqvrep  35641  bj-opabco  37941  pm11.71  45222  permaxrep  45830  upbdrech  46139  stoweidlem57  46886  or2expropbi  47923  ich2exprop  48372  ichnreuop  48373  ichreuopeq  48374  reuopreuprim  48427  pgind  50644  nfals  50733