Theorem nfex 1637

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

Syntax hints:  Ⅎwnf 1460  ∃wex 1492

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  eeor  1695  cbvexv1  1752  cbvex2  1922  eean  1931  nfsbv  1947  nfeu1  2037  nfeuv  2044  nfel  2328  ceqsex2  2777  nfopab  4071  nfopab2  4073  cbvopab1  4076  cbvopab1s  4078  repizf2  4162  copsex2t  4245  copsex2g  4246  euotd  4254  onintrab2im  4517  mosubopt  4691  nfco  4792  dfdmf  4820  dfrnf  4868  nfdm  4871  fv3  5538  nfoprab2  5924  nfoprab3  5925  nfoprab  5926  cbvoprab1  5946  cbvoprab2  5947  cbvoprab3  5950  cnvoprab  6234  ac6sfi  6897  cc3  7266  nfsum1  11363  nfsum  11364  fsum2dlemstep  11441  nfcprod1  11561  nfcprod  11562  fprod2dlemstep  11629