Theorem nfex 1661

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 1543	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbex 1660	. 2 ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
4	3	nfi 1486	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  Ⅎwnf 1484  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

This theorem depends on definitions:  df-bi 117  df-nf 1485

This theorem is referenced by:  eeor  1719  cbvexv1  1776  cbvex2  1947  eean  1960  nfsbv  1976  nfeu1  2066  nfeuv  2073  nfel  2359  ceqsex2  2818  nfopab  4128  nfopab2  4130  cbvopab1  4133  cbvopab1s  4135  repizf2  4222  copsex2t  4307  copsex2g  4308  euotd  4317  onintrab2im  4584  mosubopt  4758  nfco  4861  dfdmf  4890  dfrnf  4938  nfdm  4941  fv3  5622  nfoprab2  6018  nfoprab3  6019  nfoprab  6020  cbvoprab1  6040  cbvoprab2  6041  cbvoprab3  6044  cnvoprab  6343  ac6sfi  7021  cc3  7415  nfsum1  11782  nfsum  11783  fsum2dlemstep  11860  nfcprod1  11980  nfcprod  11981  fprod2dlemstep  12048  lss1d  14260