Theorem nfe1 2156

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

Syntax hints:  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

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

This theorem is referenced by:  nfa1  2157  nfnf1  2160  sbalex  2250  nf6  2290  exdistrf  2452  nfeu1  2590  euor2  2614  2moexv  2628  moexexvw  2629  2moswapv  2630  2euexv  2632  eupicka  2635  mopick2  2638  moexex  2639  2moex  2641  2euex  2642  2moswap  2645  2mo  2649  2eu7  2659  2eu8  2660  nfre1  3263  ceqsexg  3596  morex  3666  intab  4921  nfopab1  5156  nfopab2  5157  axrep1  5214  axrep2  5216  axrep3  5217  axrep4OLD  5220  eusv2nf  5333  copsexgw  5439  copsexg  5440  copsex2t  5441  mosubopt  5459  dfid3  5523  dmcossOLD  5926  imadif  6577  oprabidw  7392  nfoprab1  7422  nfoprab2  7423  nfoprab3  7424  zfcndrep  10531  zfcndpow  10533  zfcndreg  10534  zfcndinf  10535  reclem2pr  10965  ex-natded9.26  30507  brabgaf  32697  bnj607  35077  bnj849  35086  bnj1398  35195  bnj1449  35209  finminlem  36519  exisym1  36625  bj-alexbiex  37015  bj-exexbiex  37016  bj-biexal2  37022  bj-biexex  37025  bj-sbf3  37165  bj-axseprep  37400  bj-axreprepsep  37401  copsex2d  37472  sbexi  38451  ac6s6  38510  nfe2  42671  e2ebind  45011  e2ebindVD  45359  e2ebindALT  45376  stoweidlem57  46506  ovncvrrp  47013  ich2ex  47943  ichreuopeq  47948  reuopreuprim  48001  pgind  50207