Theorem nfex 2328

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 2328, hbex 2329. (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 1778	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1856	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2327	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1851	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1777  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by:  hbex  2329  nfnf  2330  19.12  2331  eeorOLD  2340  eean  2354  eeeanv  2356  nfmo1  2560  nfeu1  2591  moexexlem  2629  r19.12  3320  r19.12OLD  3321  ceqsex2  3547  nfopab2  5237  cbvopab1  5241  cbvopab1g  5242  cbvopab1s  5244  axrep2  5306  axrep3  5307  axrep4  5308  copsex2t  5512  mosubopt  5529  euotd  5532  nfco  5890  dfdmf  5921  dfrnf  5975  nfdm  5976  fv3  6938  oprabv  7510  nfoprab2  7512  nfoprab3  7513  nfoprab  7514  cbvoprab1  7537  cbvoprab2  7538  cbvoprab3  7541  nffrecs  8324  nfwrecsOLD  8358  ac6sfi  9348  aceq1  10186  zfcndrep  10683  zfcndinf  10687  nfsum1  15738  nfsum  15739  fsum2dlem  15818  nfcprod1  15956  nfcprod  15957  fprod2dlem  16028  brabgaf  32630  2ndresdju  32667  cnvoprabOLD  32734  bnj981  34926  bnj1388  35009  bnj1445  35020  bnj1489  35032  fineqvrep  35071  bj-opabco  37154  pm11.71  44366  upbdrech  45220  stoweidlem57  45978  or2expropbi  46949  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347  reuopreuprim  47400  pgind  48809