Theorem nfex 2324

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 2324, hbex 2325. (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 2323	. . 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 2007  ax-10 2141  ax-11 2157  ax-12 2177

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

This theorem is referenced by:  hbex  2325  nfnf  2326  19.12  2327  eeorOLD  2336  eean  2350  eeeanv  2352  ee4anv  2353  nfmo1  2557  nfeu1  2588  moexexlem  2626  r19.12  3314  r19.12OLD  3315  ceqsex2  3535  nfopab2  5214  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  axrep2  5282  axrep3  5283  axrep4OLD  5286  copsex2t  5497  mosubopt  5515  euotd  5518  nfco  5876  dfdmf  5907  dfrnf  5961  nfdm  5962  fv3  6924  oprabv  7493  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  cbvoprab1  7520  cbvoprab2  7521  cbvoprab3  7524  nffrecs  8308  nfwrecsOLD  8342  ac6sfi  9320  aceq1  10157  zfcndrep  10654  zfcndinf  10658  nfsum1  15726  nfsum  15727  fsum2dlem  15806  nfcprod1  15944  nfcprod  15945  fprod2dlem  16016  brabgaf  32620  2ndresdju  32659  bnj981  34964  bnj1388  35047  bnj1445  35058  bnj1489  35070  fineqvrep  35109  bj-opabco  37189  pm11.71  44416  upbdrech  45317  stoweidlem57  46072  or2expropbi  47046  ich2exprop  47458  ichnreuop  47459  ichreuopeq  47460  reuopreuprim  47513  pgind  49236