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 1861	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2317	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1856	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃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 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172

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

This theorem is referenced by:  hbex  2319  nfnf  2320  19.12  2321  eeorOLD  2331  eean  2345  eeeanv  2347  nfmo1  2552  nfeu1  2583  moexexlem  2623  r19.12  3312  r19.12OLD  3313  ceqsex2  3530  nfopab2  5220  cbvopab1  5224  cbvopab1g  5225  cbvopab1s  5227  axrep2  5289  axrep3  5290  axrep4  5291  copsex2t  5493  copsex2gOLD  5495  mosubopt  5511  euotd  5514  nfco  5866  dfdmf  5897  dfrnf  5950  nfdm  5951  fv3  6910  oprabv  7469  nfoprab2  7471  nfoprab3  7472  nfoprab  7473  cbvoprab1  7496  cbvoprab2  7497  cbvoprab3  7500  nffrecs  8268  nfwrecsOLD  8302  ac6sfi  9287  aceq1  10112  zfcndrep  10609  zfcndinf  10613  nfsum1  15636  nfsum  15637  fsum2dlem  15716  nfcprod1  15854  nfcprod  15855  fprod2dlem  15924  brabgaf  31837  2ndresdju  31874  cnvoprabOLD  31945  bnj981  33961  bnj1388  34044  bnj1445  34055  bnj1489  34067  fineqvrep  34095  bj-opabco  36069  pm11.71  43156  upbdrech  44015  stoweidlem57  44773  or2expropbi  45744  ich2exprop  46139  ichnreuop  46140  ichreuopeq  46141  reuopreuprim  46194  pgind  47762