Theorem nfe1 2187

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 2180	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2183	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 2178

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

This theorem is used by:  nfa1  2188  nfnf1  2191  sbalex  2278  nf6  2316  exdistrf  2476  nfeu1  2614  euor2  2638  2moexv  2652  moexexvw  2653  2moswapv  2654  2euexv  2656  eupicka  2659  mopick2  2662  moexex  2663  2moex  2665  2euex  2666  2moswap  2669  2mo  2673  2eu7  2682  2eu8  2683  nfre1  3287  ceqsexg  3607  morex  3677  intab  4938  nfopab1  5175  nfopab2  5176  axrep1  5233  axrep2  5235  axrep3  5236  axrep4OLD  5239  eusv2nf  5360  copsexgwOLD  5467  copsexg  5468  copsex2t  5469  mosubopt  5487  dfid3  5553  dmcossOLD  5960  imadif  6617  oprabidw  7444  nfoprab1  7474  nfoprab2  7475  nfoprab3  7476  zfcndrep  10623  zfcndpow  10625  zfcndreg  10626  zfcndinf  10627  reclem2pr  11057  ex-natded9.26  30899  brabgaf  33079  bnj607  35425  bnj849  35434  bnj1398  35543  bnj1449  35557  finminlem  36937  exisym1  37043  bj-alexbiex  37432  bj-exexbiex  37433  bj-biexal2  37439  bj-biexex  37442  bj-sbf3  37582  bj-axseprep  37819  bj-axreprepsep  37820  copsex2d  37891  sbexi  38861  ac6s6  38920  nfe2  43083  e2ebind  45386  e2ebindVD  45734  e2ebindALT  45751  stoweidlem57  46885  ovncvrrp  47392  ich2ex  48368  ichreuopeq  48373  reuopreuprim  48426  pgind  50643