Theorem nfe1 2147

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

Syntax hints:  ∃wex 1775  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-10 2138

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780

This theorem is referenced by:  nfa1  2148  nfnf1  2151  sbalex  2239  nf6  2281  exdistrf  2449  nfeu1ALT  2586  euor2  2610  2moexv  2624  moexexvw  2625  2moswapv  2626  2euexv  2628  eupicka  2631  mopick2  2634  moexex  2635  2moex  2637  2euex  2638  2moswap  2641  2mo  2645  2eu7  2655  2eu8  2656  nfre1  3282  ceqsexg  3652  morex  3727  intab  4982  nfopab1  5217  nfopab2  5218  axrep1  5285  axrep2  5287  axrep3  5288  axrep4OLD  5291  eusv2nf  5400  copsexgw  5500  copsexg  5501  copsex2t  5502  mosubopt  5519  dfid3  5585  dmcoss  5987  imadif  6651  oprabidw  7461  nfoprab1  7493  nfoprab2  7494  nfoprab3  7495  zfcndrep  10651  zfcndpow  10653  zfcndreg  10654  zfcndinf  10655  reclem2pr  11085  ex-natded9.26  30447  brabgaf  32627  bnj607  34908  bnj849  34917  bnj1398  35026  bnj1449  35040  finminlem  36300  exisym1  36406  bj-alexbiex  36681  bj-exexbiex  36682  bj-biexal2  36688  bj-biexex  36691  bj-sbf3  36821  copsex2d  37121  sbexi  38099  ac6s6  38158  e2ebind  44560  e2ebindVD  44909  e2ebindALT  44926  stoweidlem57  46012  ovncvrrp  46519  ich2ex  47392  ichreuopeq  47397  reuopreuprim  47450  pgind  48947