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 1777	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1855	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2322	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1855	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1850	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-11 2155  ax-12 2175

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

This theorem is referenced by:  hbex  2324  nfnf  2325  19.12  2326  eeorOLD  2335  eean  2349  eeeanv  2351  nfmo1  2555  nfeu1  2586  moexexlem  2624  r19.12  3312  r19.12OLD  3313  ceqsex2  3535  nfopab2  5219  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  axrep2  5288  axrep3  5289  axrep4OLD  5292  copsex2t  5503  mosubopt  5520  euotd  5523  nfco  5879  dfdmf  5910  dfrnf  5964  nfdm  5965  fv3  6925  oprabv  7493  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  cbvoprab1  7520  cbvoprab2  7521  cbvoprab3  7524  nffrecs  8307  nfwrecsOLD  8341  ac6sfi  9318  aceq1  10155  zfcndrep  10652  zfcndinf  10656  nfsum1  15723  nfsum  15724  fsum2dlem  15803  nfcprod1  15941  nfcprod  15942  fprod2dlem  16013  brabgaf  32628  2ndresdju  32666  cnvoprabOLD  32738  bnj981  34943  bnj1388  35026  bnj1445  35037  bnj1489  35049  fineqvrep  35088  bj-opabco  37171  pm11.71  44393  upbdrech  45256  stoweidlem57  46013  or2expropbi  46984  ich2exprop  47396  ichnreuop  47397  ichreuopeq  47398  reuopreuprim  47451  pgind  48948