Theorem nfe1 1496

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

Syntax hints:  Ⅎwnf 1460  ∃wex 1492

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 1449  ax-ie1 1493

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

This theorem is referenced by:  nf3  1669  sb4or  1833  nfmo1  2038  euexex  2111  2moswapdc  2116  nfre1  2520  ceqsexg  2865  morex  2921  sbc6g  2987  rgenm  3525  intab  3873  nfopab1  4072  nfopab2  4073  copsexg  4244  copsex2t  4245  copsex2g  4246  eusv2nf  4456  onintonm  4516  mosubopt  4691  dmcoss  4896  imadif  5296  funimaexglem  5299  nfoprab1  5923  nfoprab2  5924  nfoprab3  5925  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  dfgrp3mlem  12967