Theorem nfex 2154

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 2154, hbex 2156. (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 1705	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1784	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2153	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1784	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1779	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1481  ∃wex 1704  Ⅎwnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710

This theorem is referenced by:  hbex  2156  nfnf  2158  19.12  2164  eeor  2171  eean  2181  eeeanv  2183  nfeu1  2480  moexex  2541  ceqsex2  3244  nfopab  4718  nfopab2  4720  cbvopab1  4723  cbvopab1s  4725  axrep2  4773  axrep3  4774  axrep4  4775  copsex2t  4957  copsex2g  4958  mosubopt  4972  euotd  4975  nfco  5287  dfdmf  5317  dfrnf  5364  nfdm  5367  fv3  6206  oprabv  6703  nfoprab2  6705  nfoprab3  6706  nfoprab  6707  cbvoprab1  6727  cbvoprab2  6728  cbvoprab3  6731  nfwrecs  7409  ac6sfi  8204  aceq1  8940  zfcndrep  9436  zfcndinf  9440  nfsum1  14420  nfsum  14421  fsum2dlem  14501  nfcprod1  14640  nfcprod  14641  fprod2dlem  14710  brabgaf  29420  cnvoprab  29498  bnj981  31020  bnj1388  31101  bnj1445  31112  bnj1489  31124  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  pm11.71  38597  upbdrech  39519  stoweidlem57  40274