Theorem nfe1 1430

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

Syntax hints:  Ⅎwnf 1394  ∃wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ie1 1427

This theorem depends on definitions:  df-bi 115  df-nf 1395

This theorem is referenced by:  nf3  1604  sb4or  1761  nfmo1  1960  euexex  2033  2moswapdc  2038  nfre1  2419  ceqsexg  2743  morex  2797  sbc6g  2862  rgenm  3380  intab  3712  nfopab1  3899  nfopab2  3900  copsexg  4062  copsex2t  4063  copsex2g  4064  eusv2nf  4269  onintonm  4324  mosubopt  4491  dmcoss  4690  imadif  5080  funimaexglem  5083  nfoprab1  5680  nfoprab2  5681  nfoprab3  5682  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808