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  3262  ceqsexg  3619  morex  3690  intab  4942  nfopab1  5177  nfopab2  5178  axrep1  5235  axrep2  5237  axrep3  5238  axrep4OLD  5241  eusv2nf  5350  copsexgw  5450  copsexg  5451  copsex2t  5452  mosubopt  5470  dfid3  5536  dmcoss  5938  imadif  6600  oprabidw  7418  nfoprab1  7450  nfoprab2  7451  nfoprab3  7452  zfcndrep  10567  zfcndpow  10569  zfcndreg  10570  zfcndinf  10571  reclem2pr  11001  ex-natded9.26  30348  brabgaf  32536  bnj607  34906  bnj849  34915  bnj1398  35024  bnj1449  35038  finminlem  36306  exisym1  36412  bj-alexbiex  36687  bj-exexbiex  36688  bj-biexal2  36694  bj-biexex  36697  bj-sbf3  36827  copsex2d  37127  sbexi  38107  ac6s6  38166  e2ebind  44553  e2ebindVD  44901  e2ebindALT  44918  stoweidlem57  46055  ovncvrrp  46562  ich2ex  47469  ichreuopeq  47474  reuopreuprim  47527  pgind  49706