Theorem nfex 1573

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.)

Hypothesis

Ref	Expression
nfex.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfex	⊢ Ⅎ𝑥∃𝑦𝜑

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		nfex.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	nfri 1457	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbex 1572	. 2 ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
4	3	nfi 1396	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  Ⅎwnf 1394  ∃wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445

This theorem depends on definitions:  df-bi 115  df-nf 1395

This theorem is referenced by:  eeor  1630  cbvex2  1845  eean  1854  nfeu1  1959  nfeuv  1966  nfel  2237  ceqsex2  2659  nfopab  3898  nfopab2  3900  cbvopab1  3903  cbvopab1s  3905  repizf2  3989  copsex2t  4063  copsex2g  4064  euotd  4072  onintrab2im  4325  mosubopt  4491  nfco  4589  dfdmf  4617  dfrnf  4664  nfdm  4667  fv3  5312  nfoprab2  5681  nfoprab3  5682  nfoprab  5683  cbvoprab1  5702  cbvoprab2  5703  cbvoprab3  5706  cnvoprab  5981  ac6sfi  6594  nfsum1  10709  nfsum  10710  fsum2dlemstep  10791