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

Syntax hints:  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2141

This theorem depends on definitions:  df-bi 206  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfa1  2152  nfnf1  2155  nf6  2284  exdistrf  2449  nfeu1ALT  2591  euor2  2617  2moexv  2631  moexexvw  2632  2moswapv  2633  2euexv  2635  eupicka  2638  mopick2  2641  moexex  2642  2moex  2644  2euex  2645  2moswap  2648  2mo  2652  2eu7  2661  2eu8  2662  nfre1  3237  ceqsexg  3584  morex  3658  intab  4915  nfopab1  5149  nfopab2  5150  axrep1  5215  axrep2  5217  axrep3  5218  axrep4  5219  eusv2nf  5322  copsexgw  5407  copsexg  5408  copsex2t  5409  copsex2gOLD  5411  mosubopt  5427  dfid3  5492  dmcoss  5878  imadif  6515  oprabidw  7300  nfoprab1  7328  nfoprab2  7329  nfoprab3  7330  fsplitOLD  7947  zfcndrep  10369  zfcndpow  10371  zfcndreg  10372  zfcndinf  10373  reclem2pr  10803  ex-natded9.26  28777  brabgaf  30942  bnj607  32890  bnj849  32899  bnj1398  33008  bnj1449  33022  finminlem  34501  exisym1  34607  bj-alexbiex  34875  bj-exexbiex  34876  bj-biexal2  34882  bj-biexex  34885  bj-sbf3  35016  copsex2d  35304  sbexi  36265  ac6s6  36324  e2ebind  42151  e2ebindVD  42500  e2ebindALT  42517  stoweidlem57  43567  ovncvrrp  44071  ich2ex  44887  ichreuopeq  44892  reuopreuprim  44945