Theorem nfex 2323

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 2323, hbex 2324. (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 1780	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1857	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2322	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  hbex  2324  nfnf  2325  19.12  2326  eean  2346  eeeanv  2348  ee4anv  2349  nfmo1  2550  nfeu1  2581  moexexlem  2619  r19.12  3285  ceqsex2  3498  nfopab2  5173  cbvopab1  5176  cbvopab1g  5177  cbvopab1s  5179  axrep2  5232  axrep3  5233  axrep4OLD  5236  copsex2t  5447  mosubopt  5465  euotd  5468  nfco  5819  dfdmf  5850  dfrnf  5903  nfdm  5904  fv3  6858  oprabv  7429  nfoprab2  7431  nfoprab3  7432  nfoprab  7433  cbvoprab1  7456  cbvoprab2  7457  cbvoprab3  7460  nffrecs  8239  ac6sfi  9207  aceq1  10046  zfcndrep  10543  zfcndinf  10547  nfsum1  15632  nfsum  15633  fsum2dlem  15712  nfcprod1  15850  nfcprod  15851  fprod2dlem  15922  brabgaf  32586  2ndresdju  32623  bnj981  34933  bnj1388  35016  bnj1445  35027  bnj1489  35039  fineqvrep  35078  bj-opabco  37169  pm11.71  44379  permaxrep  44989  upbdrech  45296  stoweidlem57  46048  or2expropbi  47028  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  pgind  49699