Theorem nfe1 2156

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

Syntax hints:  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfa1  2157  nfnf1  2160  sbalex  2250  nf6  2290  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  3262  ceqsexg  3595  morex  3665  intab  4920  nfopab1  5155  nfopab2  5156  axrep1  5213  axrep2  5215  axrep3  5216  axrep4OLD  5219  eusv2nf  5337  copsexgwOLD  5444  copsexg  5445  copsex2t  5446  mosubopt  5464  dfid3  5529  dmcossOLD  5931  imadif  6582  oprabidw  7398  nfoprab1  7428  nfoprab2  7429  nfoprab3  7430  zfcndrep  10537  zfcndpow  10539  zfcndreg  10540  zfcndinf  10541  reclem2pr  10971  ex-natded9.26  30489  brabgaf  32679  bnj607  35058  bnj849  35067  bnj1398  35176  bnj1449  35190  finminlem  36500  exisym1  36606  bj-alexbiex  36996  bj-exexbiex  36997  bj-biexal2  37003  bj-biexex  37006  bj-sbf3  37146  bj-axseprep  37381  bj-axreprepsep  37382  copsex2d  37453  sbexi  38434  ac6s6  38493  nfe2  42654  e2ebind  44990  e2ebindVD  45338  e2ebindALT  45355  stoweidlem57  46485  ovncvrrp  46992  ich2ex  47928  ichreuopeq  47933  reuopreuprim  47986  pgind  50192