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  2889  morex  2945  sbc6g  3011  intab  3900  nfopab1  4099  nfopab2  4100  copsexg  4274  copsex2t  4275  copsex2g  4276  eusv2nf  4488  onintonm  4550  mosubopt  4725  dmcoss  4932  imadif  5335  funimaexglem  5338  nfoprab1  5968  nfoprab2  5969  nfoprab3  5970  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  dfgrp3mlem  13173