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  2050  euexex  2123  2moswapdc  2128  nfre1  2533  ceqsexg  2880  morex  2936  sbc6g  3002  rgenm  3540  intab  3888  nfopab1  4087  nfopab2  4088  copsexg  4262  copsex2t  4263  copsex2g  4264  eusv2nf  4474  onintonm  4534  mosubopt  4709  dmcoss  4914  imadif  5315  funimaexglem  5318  nfoprab1  5946  nfoprab2  5947  nfoprab3  5948  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  dfgrp3mlem  13057