Theorem nfex 1690

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

This proof depends on syntax axioms:  Ⅎwnf 1513  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  eeor  1747  cbvexv1  1805  cbvex2  1978  eean  1991  nfsbv  2007  nfeu1  2097  nfeuv  2104  nfel  2401  ceqsex2  2863  nfopab  4199  nfopab2  4201  cbvopab1  4204  cbvopab1s  4206  repizf2  4299  copsex2t  4385  copsex2g  4386  euotd  4395  onintrab2im  4665  mosubopt  4840  nfco  4945  dfdmf  4974  dfrnf  5023  nfdm  5026  fv3  5718  nfoprab2  6138  nfoprab3  6139  nfoprab  6140  cbvoprab1  6160  cbvoprab2  6161  cbvoprab3  6164  cnvoprab  6470  ac6sfi  7202  cc3  7635  nfsum1  12141  nfsum  12142  fsum2dlemstep  12220  nfcprod1  12340  nfcprod  12341  fprod2dlemstep  12408  lss1d  14804  nfals  17311