Theorem nfe1 1542

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

Syntax hints:  Ⅎwnf 1506  ∃wex 1538

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 1495  ax-ie1 1539

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

This theorem is referenced by:  nf3  1715  sb4or  1879  nfmo1  2089  euexex  2163  2moswapdc  2168  nfre1  2573  ceqsexg  2932  morex  2988  sbc6g  3054  intab  3955  nfopab1  4156  nfopab2  4157  copsexg  4334  copsex2t  4335  copsex2g  4336  eusv2nf  4551  onintonm  4613  mosubopt  4789  dmcoss  5000  imadif  5407  funimaexglem  5410  nfoprab1  6065  nfoprab2  6066  nfoprab3  6067  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  dfgrp3mlem  13671