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  3278  ceqsex2  3487  nfopab2  5159  cbvopab1  5162  cbvopab1g  5163  cbvopab1s  5165  axrep2  5217  axrep3  5218  axrep4OLD  5221  copsex2t  5429  mosubopt  5447  euotd  5450  nfco  5802  dfdmf  5833  dfrnf  5886  nfdm  5887  fv3  6834  oprabv  7400  nfoprab2  7402  nfoprab3  7403  nfoprab  7404  cbvoprab1  7427  cbvoprab2  7428  cbvoprab3  7431  nffrecs  8207  ac6sfi  9162  aceq1  9999  zfcndrep  10496  zfcndinf  10500  nfsum1  15584  nfsum  15585  fsum2dlem  15664  nfcprod1  15802  nfcprod  15803  fprod2dlem  15874  brabgaf  32541  2ndresdju  32583  bnj981  34930  bnj1388  35013  bnj1445  35024  bnj1489  35036  fineqvrep  35083  bj-opabco  37179  pm11.71  44387  permaxrep  44996  upbdrech  45303  stoweidlem57  46052  or2expropbi  47032  ich2exprop  47469  ichnreuop  47470  ichreuopeq  47471  reuopreuprim  47524  pgind  49716