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

Syntax hints:  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

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

This theorem is referenced by:  nfa1  2152  nfnf1  2155  sbalex  2243  nf6  2283  exdistrf  2445  nfeu1ALT  2582  euor2  2606  2moexv  2620  moexexvw  2621  2moswapv  2622  2euexv  2624  eupicka  2627  mopick2  2630  moexex  2631  2moex  2633  2euex  2634  2moswap  2637  2mo  2641  2eu7  2651  2eu8  2652  nfre1  3260  ceqsexg  3616  morex  3687  intab  4938  nfopab1  5172  nfopab2  5173  axrep1  5230  axrep2  5232  axrep3  5233  axrep4OLD  5236  eusv2nf  5345  copsexgw  5445  copsexg  5446  copsex2t  5447  mosubopt  5465  dfid3  5529  dmcoss  5927  imadif  6584  oprabidw  7400  nfoprab1  7430  nfoprab2  7431  nfoprab3  7432  zfcndrep  10543  zfcndpow  10545  zfcndreg  10546  zfcndinf  10547  reclem2pr  10977  ex-natded9.26  30398  brabgaf  32586  bnj607  34899  bnj849  34908  bnj1398  35017  bnj1449  35031  finminlem  36299  exisym1  36405  bj-alexbiex  36680  bj-exexbiex  36681  bj-biexal2  36687  bj-biexex  36690  bj-sbf3  36820  copsex2d  37120  sbexi  38100  ac6s6  38159  e2ebind  44546  e2ebindVD  44894  e2ebindALT  44911  stoweidlem57  46048  ovncvrrp  46555  ich2ex  47462  ichreuopeq  47467  reuopreuprim  47520  pgind  49699