Theorem nfex 2140

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 2140, hbex 2142. (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 1696	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1768	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2139	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1768	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1771	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701

This theorem is referenced by:  hbex  2142  nfnf  2144  19.12  2150  eeor  2157  eean  2169  eeeanv  2171  nfeu1  2468  moexex  2529  ceqsex2  3217  nfopab  4650  nfopab2  4652  cbvopab1  4655  cbvopab1s  4657  axrep2  4701  axrep3  4702  axrep4  4703  copsex2t  4883  copsex2g  4884  mosubopt  4897  euotd  4900  nfco  5209  dfdmf  5239  dfrnf  5285  nfdm  5288  fv3  6116  oprabv  6601  nfoprab2  6603  nfoprab3  6604  nfoprab  6605  cbvoprab1  6625  cbvoprab2  6626  cbvoprab3  6629  nfwrecs  7296  ac6sfi  8089  aceq1  8823  zfcndrep  9315  zfcndinf  9319  nfsum1  14268  nfsum  14269  fsum2dlem  14343  nfcprod1  14479  nfcprod  14480  fprod2dlem  14549  brabgaf  28800  cnvoprab  28886  bnj981  30274  bnj1388  30355  bnj1445  30366  bnj1489  30378  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  pm11.71  37619  upbdrech  38460  stoweidlem57  38950