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  1974  eean  1987  nfsbv  2003  nfeu1  2093  nfeuv  2100  nfel  2395  ceqsex2  2857  nfopab  4183  nfopab2  4185  cbvopab1  4188  cbvopab1s  4190  repizf2  4280  copsex2t  4366  copsex2g  4367  euotd  4376  onintrab2im  4645  mosubopt  4820  nfco  4925  dfdmf  4954  dfrnf  5003  nfdm  5006  fv3  5698  nfoprab2  6111  nfoprab3  6112  nfoprab  6113  cbvoprab1  6133  cbvoprab2  6134  cbvoprab3  6137  cnvoprab  6443  ac6sfi  7168  cc3  7598  nfsum1  12066  nfsum  12067  fsum2dlemstep  12145  nfcprod1  12265  nfcprod  12266  fprod2dlemstep  12333  lss1d  14657