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  4184  nfopab2  4186  cbvopab1  4189  cbvopab1s  4191  repizf2  4281  copsex2t  4367  copsex2g  4368  euotd  4377  onintrab2im  4647  mosubopt  4822  nfco  4927  dfdmf  4956  dfrnf  5005  nfdm  5008  fv3  5700  nfoprab2  6113  nfoprab3  6114  nfoprab  6115  cbvoprab1  6135  cbvoprab2  6136  cbvoprab3  6139  cnvoprab  6445  ac6sfi  7170  cc3  7600  nfsum1  12072  nfsum  12073  fsum2dlemstep  12151  nfcprod1  12271  nfcprod  12272  fprod2dlemstep  12339  lss1d  14663