Theorem nfex 2330

Description: If 𝑥 is not free in 𝜑, 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 2330, hbex 2332. (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 1860	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1944	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2329	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1944	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1938	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1635  ∃wex 1859  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-10 2185  ax-11 2201  ax-12 2214

This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864

This theorem is referenced by:  hbex  2332  nfnf  2334  19.12  2338  eeor  2344  eean  2355  eeeanv  2357  nfeu1  2642  moexex  2705  ceqsex2  3438  nfopab  4912  nfopab2  4914  cbvopab1  4917  cbvopab1s  4919  axrep2  4967  axrep3  4968  axrep4  4969  copsex2t  5146  copsex2g  5147  mosubopt  5165  euotd  5168  nfco  5489  dfdmf  5518  dfrnf  5565  nfdm  5568  fv3  6426  oprabv  6933  nfoprab2  6935  nfoprab3  6936  nfoprab  6937  cbvoprab1  6957  cbvoprab2  6958  cbvoprab3  6961  nfwrecs  7644  ac6sfi  8443  aceq1  9223  zfcndrep  9721  zfcndinf  9725  nfsum1  14643  nfsum  14644  fsum2dlem  14724  nfcprod1  14861  nfcprod  14862  fprod2dlem  14931  brabgaf  29745  cnvoprabOLD  29825  bnj981  31343  bnj1388  31424  bnj1445  31435  bnj1489  31447  nffrecs  32099  bj-axrep2  33103  bj-axrep3  33104  bj-axrep4  33105  pm11.71  39097  upbdrech  40000  stoweidlem57  40753