Theorem nfe1 2150

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 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 2141

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

This theorem is referenced by:  nfa1  2151  nfnf1  2154  sbalex  2242  nf6  2283  exdistrf  2452  nfeu1ALT  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  3285  ceqsexg  3653  morex  3725  intab  4978  nfopab1  5213  nfopab2  5214  axrep1  5280  axrep2  5282  axrep3  5283  axrep4OLD  5286  eusv2nf  5395  copsexgw  5495  copsexg  5496  copsex2t  5497  mosubopt  5515  dfid3  5581  dmcoss  5985  imadif  6650  oprabidw  7462  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  zfcndrep  10654  zfcndpow  10656  zfcndreg  10657  zfcndinf  10658  reclem2pr  11088  ex-natded9.26  30438  brabgaf  32620  bnj607  34930  bnj849  34939  bnj1398  35048  bnj1449  35062  finminlem  36319  exisym1  36425  bj-alexbiex  36700  bj-exexbiex  36701  bj-biexal2  36707  bj-biexex  36710  bj-sbf3  36840  copsex2d  37140  sbexi  38120  ac6s6  38179  e2ebind  44583  e2ebindVD  44932  e2ebindALT  44949  stoweidlem57  46072  ovncvrrp  46579  ich2ex  47455  ichreuopeq  47460  reuopreuprim  47513  pgind  49236