Theorem nfe1 1489

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

Syntax hints:  Ⅎwnf 1453  ∃wex 1485

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 1442  ax-ie1 1486

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

This theorem is referenced by:  nf3  1662  sb4or  1826  nfmo1  2031  euexex  2104  2moswapdc  2109  nfre1  2513  ceqsexg  2858  morex  2914  sbc6g  2979  rgenm  3517  intab  3860  nfopab1  4058  nfopab2  4059  copsexg  4229  copsex2t  4230  copsex2g  4231  eusv2nf  4441  onintonm  4501  mosubopt  4676  dmcoss  4880  imadif  5278  funimaexglem  5281  nfoprab1  5902  nfoprab2  5903  nfoprab3  5904  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180