Theorem nfex 2327

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 2327, hbex 2328. (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 2326	. . 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 2146  ax-11 2162  ax-12 2182

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

This theorem is referenced by:  hbex  2328  nfnf  2329  19.12  2330  eean  2350  eeeanv  2352  ee4anv  2353  nfmo1  2555  nfeu1  2586  moexexlem  2624  r19.12  3283  ceqsex2  3491  nfopab2  5167  cbvopab1  5170  cbvopab1g  5171  cbvopab1s  5173  axrep2  5225  axrep3  5226  axrep4OLD  5229  copsex2t  5438  mosubopt  5456  euotd  5459  nfco  5812  dfdmf  5843  dfrnf  5897  nfdm  5898  fv3  6850  oprabv  7416  nfoprab2  7418  nfoprab3  7419  nfoprab  7420  cbvoprab1  7443  cbvoprab2  7444  cbvoprab3  7447  nffrecs  8223  ac6sfi  9182  aceq1  10025  zfcndrep  10523  zfcndinf  10527  nfsum1  15611  nfsum  15612  fsum2dlem  15691  nfcprod1  15829  nfcprod  15830  fprod2dlem  15901  brabgaf  32633  2ndresdju  32676  bnj981  35055  bnj1388  35138  bnj1445  35149  bnj1489  35161  fineqvrep  35219  bj-opabco  37332  pm11.71  44580  permaxrep  45189  upbdrech  45495  stoweidlem57  46243  or2expropbi  47222  ich2exprop  47659  ichnreuop  47660  ichreuopeq  47661  reuopreuprim  47714  pgind  49904