Theorem nfex 2342

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 2342, hbex 2343. (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 1856	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2341	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1852	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1534  ∃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 1969  ax-7 2014  ax-10 2144  ax-11 2160  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1780  df-nf 1784

This theorem is referenced by:  hbex  2343  nfnf  2344  19.12  2345  eeor  2353  eean  2368  eeeanv  2370  nfmo1  2640  nfeu1  2673  moexexlem  2710  r19.12  3327  ceqsex2  3546  nfopab  5137  nfopab2  5139  cbvopab1  5142  cbvopab1g  5143  cbvopab1s  5145  axrep2  5196  axrep3  5197  axrep4  5198  copsex2t  5386  copsex2g  5387  mosubopt  5403  euotd  5406  nfco  5739  dfdmf  5768  dfrnf  5823  nfdm  5826  fv3  6691  oprabv  7217  nfoprab2  7219  nfoprab3  7220  nfoprab  7221  cbvoprab1  7244  cbvoprab2  7245  cbvoprab3  7248  nfwrecs  7952  ac6sfi  8765  aceq1  9546  zfcndrep  10039  zfcndinf  10043  nfsum1  15049  nfsumw  15050  nfsum  15051  fsum2dlem  15128  nfcprod1  15267  nfcprod  15268  fprod2dlem  15337  brabgaf  30362  cnvoprabOLD  30459  bnj981  32226  bnj1388  32309  bnj1445  32320  bnj1489  32332  nffrecs  33124  pm11.71  40735  upbdrech  41578  stoweidlem57  42349  or2expropbi  43276  ich2exprop  43640  ichnreuop  43641  ichreuopeq  43642  reuopreuprim  43695