Theorem nfe1 2155

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 2148	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2151	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfa1  2156  nfnf1  2159  sbalex  2247  nf6  2287  exdistrf  2449  nfeu1ALT  2587  euor2  2611  2moexv  2625  moexexvw  2626  2moswapv  2627  2euexv  2629  eupicka  2632  mopick2  2635  moexex  2636  2moex  2638  2euex  2639  2moswap  2642  2mo  2646  2eu7  2656  2eu8  2657  nfre1  3259  ceqsexg  3605  morex  3675  intab  4931  nfopab1  5166  nfopab2  5167  axrep1  5223  axrep2  5225  axrep3  5226  axrep4OLD  5229  eusv2nf  5338  copsexgw  5436  copsexg  5437  copsex2t  5438  mosubopt  5456  dfid3  5520  dmcossOLD  5923  imadif  6574  oprabidw  7387  nfoprab1  7417  nfoprab2  7418  nfoprab3  7419  zfcndrep  10523  zfcndpow  10525  zfcndreg  10526  zfcndinf  10527  reclem2pr  10957  ex-natded9.26  30443  brabgaf  32633  bnj607  35021  bnj849  35030  bnj1398  35139  bnj1449  35153  finminlem  36461  exisym1  36567  bj-alexbiex  36843  bj-exexbiex  36844  bj-biexal2  36850  bj-biexex  36853  bj-sbf3  36983  copsex2d  37283  sbexi  38253  ac6s6  38312  nfe2  42409  e2ebind  44746  e2ebindVD  45094  e2ebindALT  45111  stoweidlem57  46243  ovncvrrp  46750  ich2ex  47656  ichreuopeq  47661  reuopreuprim  47714  pgind  49904