Theorem nfex 1686

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

Syntax hints:  Ⅎwnf 1509  ∃wex 1541

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  eeor  1743  cbvexv1  1800  cbvex2  1971  eean  1984  nfsbv  2000  nfeu1  2090  nfeuv  2097  nfel  2384  ceqsex2  2845  nfopab  4162  nfopab2  4164  cbvopab1  4167  cbvopab1s  4169  repizf2  4258  copsex2t  4343  copsex2g  4344  euotd  4353  onintrab2im  4622  mosubopt  4797  nfco  4901  dfdmf  4930  dfrnf  4979  nfdm  4982  fv3  5671  nfoprab2  6081  nfoprab3  6082  nfoprab  6083  cbvoprab1  6103  cbvoprab2  6104  cbvoprab3  6107  cnvoprab  6408  ac6sfi  7130  cc3  7530  nfsum1  11979  nfsum  11980  fsum2dlemstep  12058  nfcprod1  12178  nfcprod  12179  fprod2dlemstep  12246  lss1d  14462