Theorem nfex 2330

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 2330, hbex 2331. (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 1782	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1859	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2329	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1859	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1855	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  hbex  2331  nfnf  2332  19.12  2333  eean  2353  eeeanv  2355  ee4anv  2356  moexexlem  2627  r19.12  3287  ceqsex2  3495  nfopab2  5171  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  axrep2  5229  axrep3  5230  axrep4OLD  5233  copsex2t  5448  mosubopt  5466  euotd  5469  nfco  5822  dfdmf  5853  dfrnf  5907  nfdm  5908  fv3  6860  oprabv  7428  nfoprab2  7430  nfoprab3  7431  nfoprab  7432  cbvoprab1  7455  cbvoprab2  7456  cbvoprab3  7459  nffrecs  8235  ac6sfi  9196  aceq1  10039  zfcndrep  10537  zfcndinf  10541  nfsum1  15625  nfsum  15626  fsum2dlem  15705  nfcprod1  15843  nfcprod  15844  fprod2dlem  15915  brabgaf  32696  2ndresdju  32739  bnj981  35126  bnj1388  35209  bnj1445  35220  bnj1489  35232  fineqvrep  35292  bj-opabco  37443  pm11.71  44753  permaxrep  45362  upbdrech  45667  stoweidlem57  46415  or2expropbi  47394  ich2exprop  47831  ichnreuop  47832  ichreuopeq  47833  reuopreuprim  47886  pgind  50076