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 1787	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1864	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2321	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1864	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1859	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1540  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-10 2141  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1787  df-nf 1791

This theorem is referenced by:  hbex  2323  nfnf  2324  19.12  2325  eeorOLD  2335  eean  2350  eeeanv  2352  nfmo1  2559  nfeu1  2590  moexexlem  2630  r19.12  3255  r19.12OLD  3256  ceqsex2  3481  nfopab2  5150  cbvopab1  5154  cbvopab1g  5155  cbvopab1s  5157  axrep2  5217  axrep3  5218  axrep4  5219  copsex2t  5410  copsex2gOLD  5412  mosubopt  5428  euotd  5431  nfco  5773  dfdmf  5804  dfrnf  5858  nfdm  5859  fv3  6789  oprabv  7330  nfoprab2  7332  nfoprab3  7333  nfoprab  7334  cbvoprab1  7357  cbvoprab2  7358  cbvoprab3  7361  nffrecs  8091  nfwrecsOLD  8125  ac6sfi  9046  aceq1  9884  zfcndrep  10381  zfcndinf  10385  nfsum1  15412  nfsum  15413  nfsumOLD  15414  fsum2dlem  15493  nfcprod1  15631  nfcprod  15632  fprod2dlem  15701  brabgaf  30957  2ndresdju  30995  cnvoprabOLD  31064  bnj981  32939  bnj1388  33022  bnj1445  33033  bnj1489  33045  fineqvrep  33073  bj-opabco  35368  pm11.71  41997  upbdrech  42826  stoweidlem57  43580  or2expropbi  44507  ich2exprop  44902  ichnreuop  44903  ichreuopeq  44904  reuopreuprim  44957