Theorem nfe1 1507

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

Syntax hints:  Ⅎwnf 1471  ∃wex 1503

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-gen 1460  ax-ie1 1504

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  nf3  1680  sb4or  1844  nfmo1  2054  euexex  2127  2moswapdc  2132  nfre1  2537  ceqsexg  2888  morex  2944  sbc6g  3010  intab  3899  nfopab1  4098  nfopab2  4099  copsexg  4273  copsex2t  4274  copsex2g  4275  eusv2nf  4487  onintonm  4549  mosubopt  4724  dmcoss  4931  imadif  5334  funimaexglem  5337  nfoprab1  5967  nfoprab2  5968  nfoprab3  5969  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  dfgrp3mlem  13170