Theorem nfe1 1440

Description: 𝑥 is not free in ∃𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfe1	⊢ Ⅎ𝑥∃𝑥𝜑

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 1439	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nfi 1406	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  Ⅎwnf 1404  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437

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

This theorem is referenced by:  nf3  1615  sb4or  1772  nfmo1  1972  euexex  2045  2moswapdc  2050  nfre1  2435  ceqsexg  2767  morex  2821  sbc6g  2886  rgenm  3412  intab  3747  nfopab1  3937  nfopab2  3938  copsexg  4104  copsex2t  4105  copsex2g  4106  eusv2nf  4315  onintonm  4371  mosubopt  4542  dmcoss  4744  imadif  5139  funimaexglem  5142  nfoprab1  5752  nfoprab2  5753  nfoprab3  5754  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968