Theorem nfe1 2151

Description: The setvar 𝑥 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 2144	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2147	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfa1  2152  nfnf1  2155  sbalex  2243  nf6  2283  exdistrf  2445  nfeu1ALT  2582  euor2  2606  2moexv  2620  moexexvw  2621  2moswapv  2622  2euexv  2624  eupicka  2627  mopick2  2630  moexex  2631  2moex  2633  2euex  2634  2moswap  2637  2mo  2641  2eu7  2651  2eu8  2652  nfre1  3254  ceqsexg  3608  morex  3679  intab  4928  nfopab1  5162  nfopab2  5163  axrep1  5219  axrep2  5221  axrep3  5222  axrep4OLD  5225  eusv2nf  5334  copsexgw  5433  copsexg  5434  copsex2t  5435  mosubopt  5453  dfid3  5517  dmcossOLD  5917  imadif  6566  oprabidw  7380  nfoprab1  7410  nfoprab2  7411  nfoprab3  7412  zfcndrep  10508  zfcndpow  10510  zfcndreg  10511  zfcndinf  10512  reclem2pr  10942  ex-natded9.26  30363  brabgaf  32553  bnj607  34883  bnj849  34892  bnj1398  35001  bnj1449  35015  finminlem  36292  exisym1  36398  bj-alexbiex  36673  bj-exexbiex  36674  bj-biexal2  36680  bj-biexex  36683  bj-sbf3  36813  copsex2d  37113  sbexi  38093  ac6s6  38152  e2ebind  44537  e2ebindVD  44885  e2ebindALT  44902  stoweidlem57  46038  ovncvrrp  46545  ich2ex  47452  ichreuopeq  47457  reuopreuprim  47510  pgind  49702