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  3288  ceqsex2  3501  nfopab2  5178  cbvopab1  5181  cbvopab1g  5182  cbvopab1s  5184  axrep2  5237  axrep3  5238  axrep4OLD  5241  copsex2t  5452  mosubopt  5470  euotd  5473  nfco  5829  dfdmf  5860  dfrnf  5914  nfdm  5915  fv3  6876  oprabv  7449  nfoprab2  7451  nfoprab3  7452  nfoprab  7453  cbvoprab1  7476  cbvoprab2  7477  cbvoprab3  7480  nffrecs  8262  ac6sfi  9231  aceq1  10070  zfcndrep  10567  zfcndinf  10571  nfsum1  15656  nfsum  15657  fsum2dlem  15736  nfcprod1  15874  nfcprod  15875  fprod2dlem  15946  brabgaf  32536  2ndresdju  32573  bnj981  34940  bnj1388  35023  bnj1445  35034  bnj1489  35046  fineqvrep  35085  bj-opabco  37176  pm11.71  44386  permaxrep  44996  upbdrech  45303  stoweidlem57  46055  or2expropbi  47035  ich2exprop  47472  ichnreuop  47473  ichreuopeq  47474  reuopreuprim  47527  pgind  49706