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

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

This theorem is referenced by:  nfa1  2148  nfnf1  2151  nf6  2279  exdistrf  2446  nfeu1ALT  2583  euor2  2609  2moexv  2623  moexexvw  2624  2moswapv  2625  2euexv  2627  eupicka  2630  mopick2  2633  moexex  2634  2moex  2636  2euex  2637  2moswap  2640  2mo  2644  2eu7  2653  2eu8  2654  nfre1  3282  ceqsexg  3641  morex  3715  intab  4982  nfopab1  5218  nfopab2  5219  axrep1  5286  axrep2  5288  axrep3  5289  axrep4  5290  eusv2nf  5393  copsexgw  5490  copsexg  5491  copsex2t  5492  copsex2gOLD  5494  mosubopt  5510  dfid3  5577  dmcoss  5970  imadif  6632  oprabidw  7439  nfoprab1  7469  nfoprab2  7470  nfoprab3  7471  zfcndrep  10608  zfcndpow  10610  zfcndreg  10611  zfcndinf  10612  reclem2pr  11042  ex-natded9.26  29669  brabgaf  31832  bnj607  33922  bnj849  33931  bnj1398  34040  bnj1449  34054  finminlem  35198  exisym1  35304  bj-alexbiex  35572  bj-exexbiex  35573  bj-biexal2  35579  bj-biexex  35582  bj-sbf3  35712  copsex2d  36015  sbexi  36976  ac6s6  37035  e2ebind  43314  e2ebindVD  43663  e2ebindALT  43680  stoweidlem57  44763  ovncvrrp  45270  ich2ex  46126  ichreuopeq  46131  reuopreuprim  46184  pgind  47752