Theorem nfe1 1472

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 1471	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nfi 1438	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  Ⅎwnf 1436  ∃wex 1468

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-gen 1425  ax-ie1 1469

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

This theorem is referenced by:  nf3  1647  sb4or  1805  nfmo1  2011  euexex  2084  2moswapdc  2089  nfre1  2476  ceqsexg  2813  morex  2868  sbc6g  2933  rgenm  3465  intab  3800  nfopab1  3997  nfopab2  3998  copsexg  4166  copsex2t  4167  copsex2g  4168  eusv2nf  4377  onintonm  4433  mosubopt  4604  dmcoss  4808  imadif  5203  funimaexglem  5206  nfoprab1  5820  nfoprab2  5821  nfoprab3  5822  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059