Theorem nfex 2312

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 2312, hbex 2313. (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 1774	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1852	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2311	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1852	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1847	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1531  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1774  df-nf 1778

This theorem is referenced by:  hbex  2313  nfnf  2314  19.12  2315  eeorOLD  2324  eean  2338  eeeanv  2340  nfmo1  2545  nfeu1  2576  moexexlem  2614  r19.12  3301  r19.12OLD  3302  ceqsex2  3519  nfopab2  5220  cbvopab1  5224  cbvopab1g  5225  cbvopab1s  5227  axrep2  5289  axrep3  5290  axrep4  5291  copsex2t  5494  copsex2gOLD  5496  mosubopt  5512  euotd  5515  nfco  5868  dfdmf  5899  dfrnf  5952  nfdm  5953  fv3  6914  oprabv  7480  nfoprab2  7482  nfoprab3  7483  nfoprab  7484  cbvoprab1  7507  cbvoprab2  7508  cbvoprab3  7511  nffrecs  8289  nfwrecsOLD  8323  ac6sfi  9315  aceq1  10147  zfcndrep  10644  zfcndinf  10648  nfsum1  15677  nfsum  15678  fsum2dlem  15757  nfcprod1  15895  nfcprod  15896  fprod2dlem  15965  brabgaf  32482  2ndresdju  32521  cnvoprabOLD  32589  bnj981  34714  bnj1388  34797  bnj1445  34808  bnj1489  34820  fineqvrep  34848  bj-opabco  36800  pm11.71  43978  upbdrech  44827  stoweidlem57  45585  or2expropbi  46556  ich2exprop  46950  ichnreuop  46951  ichreuopeq  46952  reuopreuprim  47005  pgind  48336