Theorem nfex 2357

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

Syntax hints:  ¬ wn 3  ∀wal 1568  ∃wex 1809  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by:  hbex  2358  nfnf  2359  19.12  2360  eean  2380  eeeanv  2382  ee4anv  2383  moexexlem  2654  r19.12  3314  ceqsex2  3505  nfopab2  5182  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  axrep2  5241  axrep3  5242  axrep4OLD  5245  copsex2t  5475  mosubopt  5493  euotd  5496  nfco  5851  dfdmf  5886  dfrnf  5940  nfdm  5941  fv3  6899  oprabv  7470  nfoprab2  7472  nfoprab3  7473  nfoprab  7474  cbvoprab1  7497  cbvoprab2  7498  cbvoprab3  7501  nffrecs  8276  ac6sfi  9240  aceq1  10097  zfcndrep  10594  zfcndinf  10598  nfsum1  15737  nfsum  15738  fsum2dlem  15817  nfcprod1  15958  nfcprod  15959  fprod2dlem  16030  brabgaf  32951  2ndresdju  32994  bnj981  35338  bnj1388  35421  bnj1445  35432  bnj1489  35444  fineqvrep  35527  bj-opabco  37852  pm11.71  45127  permaxrep  45735  upbdrech  46044  stoweidlem57  46791  or2expropbi  47791  ich2exprop  48240  ichnreuop  48241  ichreuopeq  48242  reuopreuprim  48295  pgind  50515  nfals  50601