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  1801  cbvex2  1972  eean  1985  nfsbv  2001  nfeu1  2091  nfeuv  2098  nfel  2393  ceqsex2  2855  nfopab  4178  nfopab2  4180  cbvopab1  4183  cbvopab1s  4185  repizf2  4275  copsex2t  4361  copsex2g  4362  euotd  4371  onintrab2im  4640  mosubopt  4815  nfco  4920  dfdmf  4949  dfrnf  4998  nfdm  5001  fv3  5693  nfoprab2  6103  nfoprab3  6104  nfoprab  6105  cbvoprab1  6125  cbvoprab2  6126  cbvoprab3  6129  cnvoprab  6430  ac6sfi  7155  cc3  7582  nfsum1  12041  nfsum  12042  fsum2dlemstep  12120  nfcprod1  12240  nfcprod  12241  fprod2dlemstep  12308  lss1d  14531