Theorem nfex 2323

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 2323, hbex 2324. (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 1857	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2322	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1538  ∃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 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  hbex  2324  nfnf  2325  19.12  2326  eean  2346  eeeanv  2348  ee4anv  2349  nfmo1  2550  nfeu1  2581  moexexlem  2619  r19.12  3278  ceqsex2  3490  nfopab2  5163  cbvopab1  5166  cbvopab1g  5167  cbvopab1s  5169  axrep2  5221  axrep3  5222  axrep4OLD  5225  copsex2t  5435  mosubopt  5453  euotd  5456  nfco  5808  dfdmf  5839  dfrnf  5892  nfdm  5893  fv3  6840  oprabv  7409  nfoprab2  7411  nfoprab3  7412  nfoprab  7413  cbvoprab1  7436  cbvoprab2  7437  cbvoprab3  7440  nffrecs  8216  ac6sfi  9173  aceq1  10011  zfcndrep  10508  zfcndinf  10512  nfsum1  15597  nfsum  15598  fsum2dlem  15677  nfcprod1  15815  nfcprod  15816  fprod2dlem  15887  brabgaf  32553  2ndresdju  32592  bnj981  34917  bnj1388  35000  bnj1445  35011  bnj1489  35023  fineqvrep  35070  bj-opabco  37166  pm11.71  44374  permaxrep  44984  upbdrech  45291  stoweidlem57  46042  or2expropbi  47022  ich2exprop  47459  ichnreuop  47460  ichreuopeq  47461  reuopreuprim  47514  pgind  49706