Theorem nfex 2324

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 2324, hbex 2325. (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 2323	. . 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 2007  ax-10 2141  ax-11 2157  ax-12 2177

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

This theorem is referenced by:  hbex  2325  nfnf  2326  19.12  2327  eeorOLD  2335  eean  2349  eeeanv  2351  ee4anv  2352  nfmo1  2556  nfeu1  2587  moexexlem  2625  r19.12  3294  ceqsex2  3514  nfopab2  5190  cbvopab1  5193  cbvopab1g  5194  cbvopab1s  5196  axrep2  5252  axrep3  5253  axrep4OLD  5256  copsex2t  5467  mosubopt  5485  euotd  5488  nfco  5845  dfdmf  5876  dfrnf  5930  nfdm  5931  fv3  6894  oprabv  7467  nfoprab2  7469  nfoprab3  7470  nfoprab  7471  cbvoprab1  7494  cbvoprab2  7495  cbvoprab3  7498  nffrecs  8282  nfwrecsOLD  8316  ac6sfi  9292  aceq1  10131  zfcndrep  10628  zfcndinf  10632  nfsum1  15706  nfsum  15707  fsum2dlem  15786  nfcprod1  15924  nfcprod  15925  fprod2dlem  15996  brabgaf  32588  2ndresdju  32627  bnj981  34981  bnj1388  35064  bnj1445  35075  bnj1489  35087  fineqvrep  35126  bj-opabco  37206  pm11.71  44421  permaxrep  45031  upbdrech  45334  stoweidlem57  46086  or2expropbi  47063  ich2exprop  47485  ichnreuop  47486  ichreuopeq  47487  reuopreuprim  47540  pgind  49581