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

Syntax hints:  ∃wex 1777  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfa1  2152  nfnf1  2155  sbalex  2243  nf6  2287  exdistrf  2455  nfeu1ALT  2592  euor2  2616  2moexv  2630  moexexvw  2631  2moswapv  2632  2euexv  2634  eupicka  2637  mopick2  2640  moexex  2641  2moex  2643  2euex  2644  2moswap  2647  2mo  2651  2eu7  2661  2eu8  2662  nfre1  3291  ceqsexg  3666  morex  3741  intab  5002  nfopab1  5236  nfopab2  5237  axrep1  5304  axrep2  5306  axrep3  5307  axrep4  5308  eusv2nf  5413  copsexgw  5510  copsexg  5511  copsex2t  5512  mosubopt  5529  dfid3  5596  dmcoss  5997  imadif  6662  oprabidw  7479  nfoprab1  7511  nfoprab2  7512  nfoprab3  7513  zfcndrep  10683  zfcndpow  10685  zfcndreg  10686  zfcndinf  10687  reclem2pr  11117  ex-natded9.26  30451  brabgaf  32630  bnj607  34892  bnj849  34901  bnj1398  35010  bnj1449  35024  finminlem  36284  exisym1  36390  bj-alexbiex  36665  bj-exexbiex  36666  bj-biexal2  36672  bj-biexex  36675  bj-sbf3  36805  copsex2d  37105  sbexi  38073  ac6s6  38132  e2ebind  44534  e2ebindVD  44883  e2ebindALT  44900  stoweidlem57  45978  ovncvrrp  46485  ich2ex  47342  ichreuopeq  47347  reuopreuprim  47400  pgind  48809