Theorem nfex 2322

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

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1783  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  hbex  2323  nfnf  2324  19.12  2325  eeor  2333  eean  2348  eeeanv  2350  nfmo1  2557  nfeu1  2588  moexexlem  2628  r19.12  3252  r19.12OLD  3253  ceqsex2  3472  nfopab2  5141  cbvopab1  5145  cbvopab1g  5146  cbvopab1s  5148  axrep2  5208  axrep3  5209  axrep4  5210  copsex2t  5400  copsex2gOLD  5402  mosubopt  5418  euotd  5421  nfco  5763  dfdmf  5794  dfrnf  5848  nfdm  5849  fv3  6774  oprabv  7313  nfoprab2  7315  nfoprab3  7316  nfoprab  7317  cbvoprab1  7340  cbvoprab2  7341  cbvoprab3  7344  nffrecs  8070  nfwrecsOLD  8104  ac6sfi  8988  aceq1  9804  zfcndrep  10301  zfcndinf  10305  nfsum1  15329  nfsum  15330  nfsumOLD  15331  fsum2dlem  15410  nfcprod1  15548  nfcprod  15549  fprod2dlem  15618  brabgaf  30849  2ndresdju  30887  cnvoprabOLD  30957  bnj981  32830  bnj1388  32913  bnj1445  32924  bnj1489  32936  fineqvrep  32964  bj-opabco  35286  pm11.71  41904  upbdrech  42734  stoweidlem57  43488  or2expropbi  44415  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866