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  3952  nfopab1  4153  nfopab2  4154  copsexg  4330  copsex2t  4331  copsex2g  4332  eusv2nf  4547  onintonm  4609  mosubopt  4784  dmcoss  4994  imadif  5401  funimaexglem  5404  nfoprab1  6059  nfoprab2  6060  nfoprab3  6061  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  dfgrp3mlem  13646