Theorem nfe1 2188

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

This proof depends on syntax axioms:  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2179

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfa1  2189  nfnf1  2192  sbalex  2281  nf6  2320  exdistrf  2481  nfeu1  2619  euor2  2643  2moexv  2657  moexexvw  2658  2moswapv  2659  2euexv  2661  eupicka  2664  mopick2  2667  moexex  2668  2moex  2670  2euex  2671  2moswap  2674  2mo  2678  2eu7  2687  2eu8  2688  nfre1  3292  ceqsexg  3614  morex  3684  intab  4945  nfopab1  5183  nfopab2  5184  axrep1  5241  axrep2  5243  axrep3  5244  axrep4OLD  5247  eusv2nf  5368  copsexgwOLD  5475  copsexg  5476  copsex2t  5477  mosubopt  5495  dfid3  5561  dmcossOLD  5968  imadif  6624  oprabidw  7450  nfoprab1  7480  nfoprab2  7481  nfoprab3  7482  zfcndrep  10614  zfcndpow  10616  zfcndreg  10617  zfcndinf  10618  reclem2pr  11048  ex-natded9.26  30841  brabgaf  33022  bnj607  35369  bnj849  35378  bnj1398  35487  bnj1449  35501  finminlem  36886  exisym1  36992  bj-alexbiex  37381  bj-exexbiex  37382  bj-biexal2  37388  bj-biexex  37391  bj-sbf3  37531  bj-axseprep  37768  bj-axreprepsep  37769  copsex2d  37840  sbexi  38820  ac6s6  38879  nfe2  43042  e2ebind  45330  e2ebindVD  45678  e2ebindALT  45695  stoweidlem57  46829  ovncvrrp  47336  ich2ex  48275  ichreuopeq  48280  reuopreuprim  48333  pgind  50552