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  30321  brabgaf  32509  bnj607  34879  bnj849  34888  bnj1398  34997  bnj1449  35011  finminlem  36279  exisym1  36385  bj-alexbiex  36660  bj-exexbiex  36661  bj-biexal2  36667  bj-biexex  36670  bj-sbf3  36800  copsex2d  37100  sbexi  38080  ac6s6  38139  e2ebind  44526  e2ebindVD  44874  e2ebindALT  44891  stoweidlem57  46028  ovncvrrp  46535  ich2ex  47442  ichreuopeq  47447  reuopreuprim  47500  pgind  49679