Theorem nfex 1683

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

Syntax hints:  Ⅎwnf 1506  ∃wex 1538

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  eeor  1741  cbvexv1  1798  cbvex2  1969  eean  1982  nfsbv  1998  nfeu1  2088  nfeuv  2095  nfel  2381  ceqsex2  2841  nfopab  4152  nfopab2  4154  cbvopab1  4157  cbvopab1s  4159  repizf2  4246  copsex2t  4331  copsex2g  4332  euotd  4341  onintrab2im  4610  mosubopt  4784  nfco  4887  dfdmf  4916  dfrnf  4965  nfdm  4968  fv3  5652  nfoprab2  6060  nfoprab3  6061  nfoprab  6062  cbvoprab1  6082  cbvoprab2  6083  cbvoprab3  6086  cnvoprab  6386  ac6sfi  7068  cc3  7465  nfsum1  11882  nfsum  11883  fsum2dlemstep  11960  nfcprod1  12080  nfcprod  12081  fprod2dlemstep  12148  lss1d  14362