Theorem nfex 1617

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

Syntax hints:  Ⅎwnf 1437  ∃wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  eeor  1674  cbvex2  1895  eean  1904  nfeu1  2011  nfeuv  2018  nfel  2291  ceqsex2  2729  nfopab  4004  nfopab2  4006  cbvopab1  4009  cbvopab1s  4011  repizf2  4094  copsex2t  4175  copsex2g  4176  euotd  4184  onintrab2im  4442  mosubopt  4612  nfco  4712  dfdmf  4740  dfrnf  4788  nfdm  4791  fv3  5452  nfoprab2  5829  nfoprab3  5830  nfoprab  5831  cbvoprab1  5851  cbvoprab2  5852  cbvoprab3  5855  cnvoprab  6139  ac6sfi  6800  cc3  7100  nfsum1  11157  nfsum  11158  fsum2dlemstep  11235  nfcprod1  11355  nfcprod  11356