Theorem nfex 2318

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 2318, hbex 2319. (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 1783	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1860	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2317	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1860	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1855	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  hbex  2319  nfnf  2320  19.12  2321  eeorOLD  2331  eean  2346  eeeanv  2348  nfmo1  2557  nfeu1  2588  moexexlem  2628  r19.12  3257  r19.12OLD  3258  ceqsex2  3482  nfopab2  5145  cbvopab1  5149  cbvopab1g  5150  cbvopab1s  5152  axrep2  5212  axrep3  5213  axrep4  5214  copsex2t  5406  copsex2gOLD  5408  mosubopt  5424  euotd  5427  nfco  5774  dfdmf  5805  dfrnf  5859  nfdm  5860  fv3  6792  oprabv  7335  nfoprab2  7337  nfoprab3  7338  nfoprab  7339  cbvoprab1  7362  cbvoprab2  7363  cbvoprab3  7366  nffrecs  8099  nfwrecsOLD  8133  ac6sfi  9058  aceq1  9873  zfcndrep  10370  zfcndinf  10374  nfsum1  15401  nfsum  15402  nfsumOLD  15403  fsum2dlem  15482  nfcprod1  15620  nfcprod  15621  fprod2dlem  15690  brabgaf  30948  2ndresdju  30986  cnvoprabOLD  31055  bnj981  32930  bnj1388  33013  bnj1445  33024  bnj1489  33036  fineqvrep  33064  bj-opabco  35359  pm11.71  42015  upbdrech  42844  stoweidlem57  43598  or2expropbi  44528  ich2exprop  44923  ichnreuop  44924  ichreuopeq  44925  reuopreuprim  44978