Theorem nfex 2325

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 2325, hbex 2326. (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 1781	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1858	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2324	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  hbex  2326  nfnf  2327  19.12  2328  eean  2348  eeeanv  2350  ee4anv  2351  nfmo1  2552  nfeu1  2583  moexexlem  2621  r19.12  3281  ceqsex2  3489  nfopab2  5160  cbvopab1  5163  cbvopab1g  5164  cbvopab1s  5166  axrep2  5218  axrep3  5219  axrep4OLD  5222  copsex2t  5430  mosubopt  5448  euotd  5451  nfco  5804  dfdmf  5835  dfrnf  5889  nfdm  5890  fv3  6840  oprabv  7406  nfoprab2  7408  nfoprab3  7409  nfoprab  7410  cbvoprab1  7433  cbvoprab2  7434  cbvoprab3  7437  nffrecs  8213  ac6sfi  9168  aceq1  10008  zfcndrep  10505  zfcndinf  10509  nfsum1  15597  nfsum  15598  fsum2dlem  15677  nfcprod1  15815  nfcprod  15816  fprod2dlem  15887  brabgaf  32589  2ndresdju  32631  bnj981  34962  bnj1388  35045  bnj1445  35056  bnj1489  35068  fineqvrep  35137  bj-opabco  37232  pm11.71  44500  permaxrep  45109  upbdrech  45416  stoweidlem57  46165  or2expropbi  47144  ich2exprop  47581  ichnreuop  47582  ichreuopeq  47583  reuopreuprim  47636  pgind  49828