Theorem nfex 1660

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

Syntax hints:  Ⅎwnf 1483  ∃wex 1515

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533

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

This theorem is referenced by:  eeor  1718  cbvexv1  1775  cbvex2  1946  eean  1959  nfsbv  1975  nfeu1  2065  nfeuv  2072  nfel  2357  ceqsex2  2813  nfopab  4112  nfopab2  4114  cbvopab1  4117  cbvopab1s  4119  repizf2  4206  copsex2t  4289  copsex2g  4290  euotd  4299  onintrab2im  4566  mosubopt  4740  nfco  4843  dfdmf  4871  dfrnf  4919  nfdm  4922  fv3  5599  nfoprab2  5995  nfoprab3  5996  nfoprab  5997  cbvoprab1  6017  cbvoprab2  6018  cbvoprab3  6021  cnvoprab  6320  ac6sfi  6995  cc3  7380  nfsum1  11667  nfsum  11668  fsum2dlemstep  11745  nfcprod1  11865  nfcprod  11866  fprod2dlemstep  11933  lss1d  14145