Theorem nfex 2317

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

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃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 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 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  hbex  2318  nfnf  2319  19.12  2320  eeorOLD  2330  eean  2344  eeeanv  2346  nfmo1  2551  nfeu1  2582  moexexlem  2622  r19.12  3311  r19.12OLD  3312  ceqsex2  3529  nfopab2  5218  cbvopab1  5222  cbvopab1g  5223  cbvopab1s  5225  axrep2  5287  axrep3  5288  axrep4  5289  copsex2t  5491  copsex2gOLD  5493  mosubopt  5509  euotd  5512  nfco  5863  dfdmf  5894  dfrnf  5947  nfdm  5948  fv3  6906  oprabv  7465  nfoprab2  7467  nfoprab3  7468  nfoprab  7469  cbvoprab1  7492  cbvoprab2  7493  cbvoprab3  7496  nffrecs  8264  nfwrecsOLD  8298  ac6sfi  9283  aceq1  10108  zfcndrep  10605  zfcndinf  10609  nfsum1  15632  nfsum  15633  fsum2dlem  15712  nfcprod1  15850  nfcprod  15851  fprod2dlem  15920  brabgaf  31824  2ndresdju  31861  cnvoprabOLD  31932  bnj981  33949  bnj1388  34032  bnj1445  34043  bnj1489  34055  fineqvrep  34083  bj-opabco  36057  pm11.71  43141  upbdrech  44001  stoweidlem57  44759  or2expropbi  45730  ich2exprop  46125  ichnreuop  46126  ichreuopeq  46127  reuopreuprim  46180  pgind  47715