Theorem nfex 2356

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 2356, hbex 2357. (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 1813	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1890	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2355	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1886	1 ⊢ Ⅎ𝑥∃𝑦𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2215

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  hbex  2357  nfnf  2358  19.12  2359  eean  2379  eeeanv  2381  ee4anv  2382  moexexlem  2653  r19.12  3313  ceqsex2  3503  nfopab2  5180  cbvopab1  5183  cbvopab1g  5184  cbvopab1s  5186  axrep2  5239  axrep3  5240  axrep4OLD  5243  copsex2t  5473  mosubopt  5491  euotd  5494  nfco  5849  dfdmf  5884  dfrnf  5938  nfdm  5939  fv3  6900  oprabv  7477  nfoprab2  7479  nfoprab3  7480  nfoprab  7481  cbvoprab1  7504  cbvoprab2  7505  cbvoprab3  7508  nffrecs  8286  ac6sfi  9258  aceq1  10124  zfcndrep  10627  zfcndinf  10631  nfsum1  15781  nfsum  15782  fsum2dlem  15860  nfcprod1  16001  nfcprod  16002  fprod2dlem  16073  brabgaf  33087  2ndresdju  33130  bnj981  35467  bnj1388  35550  bnj1445  35561  bnj1489  35573  fineqvrep  35648  bj-opabco  37948  pm11.71  45229  permaxrep  45837  upbdrech  46146  stoweidlem57  46893  or2expropbi  47930  ich2exprop  48379  ichnreuop  48380  ichreuopeq  48381  reuopreuprim  48434  pgind  50651  nfals  50740