Theorem nfe1 1518

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

Syntax hints:  Ⅎwnf 1482  ∃wex 1514

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 1471  ax-ie1 1515

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

This theorem is referenced by:  nf3  1691  sb4or  1855  nfmo1  2065  euexex  2138  2moswapdc  2143  nfre1  2548  ceqsexg  2900  morex  2956  sbc6g  3022  intab  3913  nfopab1  4112  nfopab2  4113  copsexg  4287  copsex2t  4288  copsex2g  4289  eusv2nf  4501  onintonm  4563  mosubopt  4738  dmcoss  4945  imadif  5348  funimaexglem  5351  nfoprab1  5984  nfoprab2  5985  nfoprab3  5986  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  dfgrp3mlem  13348