Theorem nfex 2356

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 2356, hbex 2357. (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 1800	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1877	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2355	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1877	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1873	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1558  ∃wex 1799  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-10 2175  ax-11 2191  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1800  df-nf 1804

This theorem is referenced by:  hbex  2357  nfnf  2358  19.12  2359  eean  2379  eeeanv  2381  ee4anv  2382  moexexlem  2653  r19.12  3311  ceqsex2  3504  nfopab2  5171  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  axrep2  5230  axrep3  5231  axrep4OLD  5234  copsex2t  5461  mosubopt  5479  euotd  5482  nfco  5837  dfdmf  5872  dfrnf  5926  nfdm  5927  fv3  6885  oprabv  7456  nfoprab2  7458  nfoprab3  7459  nfoprab  7460  cbvoprab1  7483  cbvoprab2  7484  cbvoprab3  7487  nffrecs  8264  ac6sfi  9228  aceq1  10073  zfcndrep  10572  zfcndinf  10576  nfsum1  15717  nfsum  15718  fsum2dlem  15797  nfcprod1  15938  nfcprod  15939  fprod2dlem  16010  brabgaf  32808  2ndresdju  32851  bnj981  35245  bnj1388  35328  bnj1445  35339  bnj1489  35351  fineqvrep  35410  bj-opabco  37680  pm11.71  44973  permaxrep  45582  upbdrech  45884  stoweidlem57  46631  or2expropbi  47628  ich2exprop  48077  ichnreuop  48078  ichreuopeq  48079  reuopreuprim  48132  pgind  50338