Theorem nfe1 2145

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

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

This theorem is referenced by:  nfa1  2146  nfnf1  2149  nf6  2277  exdistrf  2444  nfeu1ALT  2581  euor2  2607  2moexv  2621  moexexvw  2622  2moswapv  2623  2euexv  2625  eupicka  2628  mopick2  2631  moexex  2632  2moex  2634  2euex  2635  2moswap  2638  2mo  2642  2eu7  2651  2eu8  2652  nfre1  3280  ceqsexg  3642  morex  3716  intab  4983  nfopab1  5219  nfopab2  5220  axrep1  5287  axrep2  5289  axrep3  5290  axrep4  5291  eusv2nf  5394  copsexgw  5491  copsexg  5492  copsex2t  5493  copsex2gOLD  5495  mosubopt  5511  dfid3  5578  dmcoss  5971  imadif  6633  oprabidw  7444  nfoprab1  7474  nfoprab2  7475  nfoprab3  7476  zfcndrep  10613  zfcndpow  10615  zfcndreg  10616  zfcndinf  10617  reclem2pr  11047  ex-natded9.26  29937  brabgaf  32102  bnj607  34223  bnj849  34232  bnj1398  34341  bnj1449  34355  finminlem  35508  exisym1  35614  bj-alexbiex  35882  bj-exexbiex  35883  bj-biexal2  35889  bj-biexex  35892  bj-sbf3  36022  copsex2d  36325  sbexi  37286  ac6s6  37345  e2ebind  43628  e2ebindVD  43977  e2ebindALT  43994  stoweidlem57  45073  ovncvrrp  45580  ich2ex  46436  ichreuopeq  46441  reuopreuprim  46494  pgind  47851