Theorem nfex 1617

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

Syntax hints:  Ⅎwnf 1440  ∃wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490

This theorem depends on definitions:  df-bi 116  df-nf 1441

This theorem is referenced by:  eeor  1675  cbvexv1  1732  cbvex2  1902  eean  1911  nfsbv  1927  nfeu1  2017  nfeuv  2024  nfel  2308  ceqsex2  2752  nfopab  4032  nfopab2  4034  cbvopab1  4037  cbvopab1s  4039  repizf2  4123  copsex2t  4205  copsex2g  4206  euotd  4214  onintrab2im  4477  mosubopt  4651  nfco  4751  dfdmf  4779  dfrnf  4827  nfdm  4830  fv3  5491  nfoprab2  5871  nfoprab3  5872  nfoprab  5873  cbvoprab1  5893  cbvoprab2  5894  cbvoprab3  5897  cnvoprab  6181  ac6sfi  6843  cc3  7188  nfsum1  11253  nfsum  11254  fsum2dlemstep  11331  nfcprod1  11451  nfcprod  11452  fprod2dlemstep  11519