Theorem nfex 2357

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-10 2179  ax-11 2196  ax-12 2215

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  hbex  2358  nfnf  2359  19.12  2360  eean  2380  eeeanv  2382  ee4anv  2383  moexexlem  2654  r19.12  3314  ceqsex2  3503  nfopab2  5178  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  axrep2  5237  axrep3  5238  copsex2t  5467  mosubopt  5485  mosubott  5487  euotd  5489  nfco  5847  dfdmf  5882  dfrnf  5936  nfdm  5937  fv3  6911  oprabv  7487  nfoprab2  7489  nfoprab3  7490  nfoprab  7491  cbvoprab1  7514  cbvoprab2  7515  cbvoprab3  7518  nffrecs  8312  ac6sfi  9286  aceq1  10206  zfcndrep  10709  zfcndinf  10713  nfsum1  15869  nfsum  15870  fsum2dlem  15948  nfcprod1  16089  nfcprod  16090  fprod2dlem  16159  brabgaf  33254  2ndresdju  33297  bnj981  35633  bnj1388  35716  bnj1445  35727  bnj1489  35739  fineqvrep  35853  bj-opabco  38249  pm11.71  45521  permaxrep  46135  upbdrech  46460  stoweidlem57  47206  or2expropbi  48243  ich2exprop  48692  ichnreuop  48693  ichreuopeq  48694  reuopreuprim  48747  pgind  51024  nfals  51113