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  4151  nfopab2  4153  cbvopab1  4156  cbvopab1s  4158  repizf2  4245  copsex2t  4330  copsex2g  4331  euotd  4340  onintrab2im  4609  mosubopt  4783  nfco  4886  dfdmf  4915  dfrnf  4964  nfdm  4967  fv3  5649  nfoprab2  6053  nfoprab3  6054  nfoprab  6055  cbvoprab1  6075  cbvoprab2  6076  cbvoprab3  6079  cnvoprab  6378  ac6sfi  7056  cc3  7450  nfsum1  11862  nfsum  11863  fsum2dlemstep  11940  nfcprod1  12060  nfcprod  12061  fprod2dlemstep  12128  lss1d  14341