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  2931  morex  2987  sbc6g  3053  intab  3951  nfopab1  4152  nfopab2  4153  copsexg  4329  copsex2t  4330  copsex2g  4331  eusv2nf  4546  onintonm  4608  mosubopt  4783  dmcoss  4993  imadif  5400  funimaexglem  5403  nfoprab1  6052  nfoprab2  6053  nfoprab3  6054  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  dfgrp3mlem  13626