Theorem nfe1 2149

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

Syntax hints:  ∃wex 1778  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-10 2140

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  nfa1  2150  nfnf1  2153  sbalex  2241  nf6  2282  exdistrf  2450  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  3265  ceqsexg  3630  morex  3700  intab  4951  nfopab1  5186  nfopab2  5187  axrep1  5247  axrep2  5249  axrep3  5250  axrep4OLD  5253  eusv2nf  5362  copsexgw  5462  copsexg  5463  copsex2t  5464  mosubopt  5482  dfid3  5548  dmcoss  5951  imadif  6616  oprabidw  7430  nfoprab1  7462  nfoprab2  7463  nfoprab3  7464  zfcndrep  10620  zfcndpow  10622  zfcndreg  10623  zfcndinf  10624  reclem2pr  11054  ex-natded9.26  30332  brabgaf  32521  bnj607  34868  bnj849  34877  bnj1398  34986  bnj1449  35000  finminlem  36257  exisym1  36363  bj-alexbiex  36638  bj-exexbiex  36639  bj-biexal2  36645  bj-biexex  36648  bj-sbf3  36778  copsex2d  37078  sbexi  38058  ac6s6  38117  e2ebind  44514  e2ebindVD  44863  e2ebindALT  44880  stoweidlem57  46016  ovncvrrp  46523  ich2ex  47400  ichreuopeq  47405  reuopreuprim  47458  pgind  49301