Theorem nfe1 1385

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

Syntax hints:  Ⅎwnf 1349  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie1 1382

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nf3  1559  sb4or  1714  nfmo1  1912  euexex  1985  2moswapdc  1990  nfre1  2365  ceqsexg  2672  morex  2725  sbc6g  2788  rgenm  3323  intab  3644  nfopab1  3826  nfopab2  3827  copsexg  3981  copsex2t  3982  copsex2g  3983  eusv2nf  4188  onintonm  4243  mosubopt  4405  dmcoss  4601  imadif  4979  funimaexglem  4982  nfoprab1  5554  nfoprab2  5555  nfoprab3  5556