Theorem nfex 2363

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 2363, hbex 2364. (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 1807	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1884	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2362	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1884	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1880	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1565  ∃wex 1806  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1807  df-nf 1811

This theorem is referenced by:  hbex  2364  nfnf  2365  19.12  2366  eean  2386  eeeanv  2388  ee4anv  2389  moexexlem  2660  r19.12  3320  ceqsex2  3513  nfopab2  5186  cbvopab1  5189  cbvopab1g  5190  cbvopab1s  5192  axrep2  5245  axrep3  5246  axrep4OLD  5249  copsex2t  5476  mosubopt  5494  euotd  5497  nfco  5852  dfdmf  5887  dfrnf  5941  nfdm  5942  fv3  6900  oprabv  7471  nfoprab2  7473  nfoprab3  7474  nfoprab  7475  cbvoprab1  7498  cbvoprab2  7499  cbvoprab3  7502  nffrecs  8280  ac6sfi  9244  aceq1  10101  zfcndrep  10599  zfcndinf  10603  nfsum1  15741  nfsum  15742  fsum2dlem  15821  nfcprod1  15962  nfcprod  15963  fprod2dlem  16034  brabgaf  32892  2ndresdju  32935  bnj981  35283  bnj1388  35366  bnj1445  35377  bnj1489  35389  fineqvrep  35450  bj-opabco  37720  pm11.71  44999  permaxrep  45607  upbdrech  45916  stoweidlem57  46663  or2expropbi  47660  ich2exprop  48109  ichnreuop  48110  ichreuopeq  48111  reuopreuprim  48164  pgind  50380  nfals  50466