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  2551  nfeu1  2582  moexexlem  2620  r19.12  3290  ceqsex2  3504  nfopab2  5181  cbvopab1  5184  cbvopab1g  5185  cbvopab1s  5187  axrep2  5240  axrep3  5241  axrep4OLD  5244  copsex2t  5455  mosubopt  5473  euotd  5476  nfco  5832  dfdmf  5863  dfrnf  5917  nfdm  5918  fv3  6879  oprabv  7452  nfoprab2  7454  nfoprab3  7455  nfoprab  7456  cbvoprab1  7479  cbvoprab2  7480  cbvoprab3  7483  nffrecs  8265  ac6sfi  9238  aceq1  10077  zfcndrep  10574  zfcndinf  10578  nfsum1  15663  nfsum  15664  fsum2dlem  15743  nfcprod1  15881  nfcprod  15882  fprod2dlem  15953  brabgaf  32543  2ndresdju  32580  bnj981  34947  bnj1388  35030  bnj1445  35041  bnj1489  35053  fineqvrep  35092  bj-opabco  37183  pm11.71  44393  permaxrep  45003  upbdrech  45310  stoweidlem57  46062  or2expropbi  47039  ich2exprop  47476  ichnreuop  47477  ichreuopeq  47478  reuopreuprim  47531  pgind  49710