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  3609  morex  3679  intab  4935  nfopab1  5170  nfopab2  5171  axrep1  5227  axrep2  5229  axrep3  5230  axrep4OLD  5233  eusv2nf  5342  copsexgw  5446  copsexg  5447  copsex2t  5448  mosubopt  5466  dfid3  5530  dmcossOLD  5933  imadif  6584  oprabidw  7399  nfoprab1  7429  nfoprab2  7430  nfoprab3  7431  zfcndrep  10537  zfcndpow  10539  zfcndreg  10540  zfcndinf  10541  reclem2pr  10971  ex-natded9.26  30506  brabgaf  32696  bnj607  35092  bnj849  35101  bnj1398  35210  bnj1449  35224  finminlem  36534  exisym1  36640  bj-alexbiex  36944  bj-exexbiex  36945  bj-biexal2  36951  bj-biexex  36954  bj-sbf3  37087  bj-axseprep  37322  bj-axreprepsep  37323  copsex2d  37394  sbexi  38364  ac6s6  38423  nfe2  42585  e2ebind  44919  e2ebindVD  45267  e2ebindALT  45284  stoweidlem57  46415  ovncvrrp  46922  ich2ex  47828  ichreuopeq  47833  reuopreuprim  47886  pgind  50076