Theorem nfe1 1510

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

Syntax hints:  Ⅎwnf 1474  ∃wex 1506

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 1463  ax-ie1 1507

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

This theorem is referenced by:  nf3  1683  sb4or  1847  nfmo1  2057  euexex  2130  2moswapdc  2135  nfre1  2540  ceqsexg  2892  morex  2948  sbc6g  3014  intab  3904  nfopab1  4103  nfopab2  4104  copsexg  4278  copsex2t  4279  copsex2g  4280  eusv2nf  4492  onintonm  4554  mosubopt  4729  dmcoss  4936  imadif  5339  funimaexglem  5342  nfoprab1  5975  nfoprab2  5976  nfoprab3  5977  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  dfgrp3mlem  13300