Theorem nfex 2332

Description: If 𝑥 is not free in 𝜑, 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 2332, hbex 2333. (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 1782	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1858	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2331	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by:  hbex  2333  nfnf  2334  19.12  2335  eeor  2343  eean  2358  eeeanv  2360  nfmo1  2616  nfeu1  2649  moexexlem  2688  r19.12  3283  ceqsex2  3491  nfopab  5098  nfopab2  5100  cbvopab1  5103  cbvopab1g  5104  cbvopab1s  5106  axrep2  5157  axrep3  5158  axrep4  5159  copsex2t  5348  copsex2g  5349  mosubopt  5365  euotd  5368  nfco  5700  dfdmf  5729  dfrnf  5784  nfdm  5787  fv3  6663  oprabv  7193  nfoprab2  7195  nfoprab3  7196  nfoprab  7197  cbvoprab1  7220  cbvoprab2  7221  cbvoprab3  7224  nfwrecs  7932  ac6sfi  8746  aceq1  9528  zfcndrep  10025  zfcndinf  10029  nfsum1  15038  nfsum  15039  nfsumOLD  15040  fsum2dlem  15117  nfcprod1  15256  nfcprod  15257  fprod2dlem  15326  brabgaf  30372  2ndresdju  30411  cnvoprabOLD  30482  bnj981  32332  bnj1388  32415  bnj1445  32426  bnj1489  32438  nffrecs  33233  bj-opabco  34603  pm11.71  41101  upbdrech  41937  stoweidlem57  42699  or2expropbi  43626  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990  reuopreuprim  44043