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  2842  nfopab  4155  nfopab2  4157  cbvopab1  4160  cbvopab1s  4162  repizf2  4250  copsex2t  4335  copsex2g  4336  euotd  4345  onintrab2im  4614  mosubopt  4789  nfco  4893  dfdmf  4922  dfrnf  4971  nfdm  4974  fv3  5658  nfoprab2  6066  nfoprab3  6067  nfoprab  6068  cbvoprab1  6088  cbvoprab2  6089  cbvoprab3  6092  cnvoprab  6394  ac6sfi  7080  cc3  7477  nfsum1  11907  nfsum  11908  fsum2dlemstep  11985  nfcprod1  12105  nfcprod  12106  fprod2dlemstep  12173  lss1d  14387