Theorem nfex 1659

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

Syntax hints:  Ⅎwnf 1482  ∃wex 1514

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532

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

This theorem is referenced by:  eeor  1717  cbvexv1  1774  cbvex2  1945  eean  1958  nfsbv  1974  nfeu1  2064  nfeuv  2071  nfel  2356  ceqsex2  2812  nfopab  4111  nfopab2  4113  cbvopab1  4116  cbvopab1s  4118  repizf2  4205  copsex2t  4288  copsex2g  4289  euotd  4298  onintrab2im  4565  mosubopt  4739  nfco  4842  dfdmf  4870  dfrnf  4918  nfdm  4921  fv3  5598  nfoprab2  5994  nfoprab3  5995  nfoprab  5996  cbvoprab1  6016  cbvoprab2  6017  cbvoprab3  6020  cnvoprab  6319  ac6sfi  6994  cc3  7379  nfsum1  11638  nfsum  11639  fsum2dlemstep  11716  nfcprod1  11836  nfcprod  11837  fprod2dlemstep  11904  lss1d  14116