Theorem nfe1 2155

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

Syntax hints:  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfa1  2156  nfnf1  2159  sbalex  2249  nf6  2289  exdistrf  2451  nfeu1  2589  euor2  2613  2moexv  2627  moexexvw  2628  2moswapv  2629  2euexv  2631  eupicka  2634  mopick2  2637  moexex  2638  2moex  2640  2euex  2641  2moswap  2644  2mo  2648  2eu7  2658  2eu8  2659  nfre1  3261  ceqsexg  3607  morex  3677  intab  4933  nfopab1  5168  nfopab2  5169  axrep1  5225  axrep2  5227  axrep3  5228  axrep4OLD  5231  eusv2nf  5340  copsexgw  5438  copsexg  5439  copsex2t  5440  mosubopt  5458  dfid3  5522  dmcossOLD  5925  imadif  6576  oprabidw  7389  nfoprab1  7419  nfoprab2  7420  nfoprab3  7421  zfcndrep  10525  zfcndpow  10527  zfcndreg  10528  zfcndinf  10529  reclem2pr  10959  ex-natded9.26  30494  brabgaf  32684  bnj607  35072  bnj849  35081  bnj1398  35190  bnj1449  35204  finminlem  36512  exisym1  36618  bj-alexbiex  36900  bj-exexbiex  36901  bj-biexal2  36907  bj-biexex  36910  bj-sbf3  37040  copsex2d  37344  sbexi  38314  ac6s6  38373  nfe2  42469  e2ebind  44804  e2ebindVD  45152  e2ebindALT  45169  stoweidlem57  46301  ovncvrrp  46808  ich2ex  47714  ichreuopeq  47719  reuopreuprim  47772  pgind  49962