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  2279  nf6  2317  exdistrf  2477  nfeu1  2615  euor2  2639  2moexv  2653  moexexvw  2654  2moswapv  2655  2euexv  2657  eupicka  2660  mopick2  2663  moexex  2664  2moex  2666  2euex  2667  2moswap  2670  2mo  2674  2eu7  2683  2eu8  2684  nfre1  3288  ceqsexg  3607  morex  3677  intab  4938  nfopab1  5175  nfopab2  5176  axrep1  5233  axrep2  5235  axrep3  5236  eusv2nf  5357  copsexgwOLD  5461  copsexg  5462  copsex2t  5464  mosubopt  5482  mosubott  5484  dfid3  5549  dmcossOLD  5958  imadif  6622  oprabidw  7449  nfoprab1  7479  nfoprab2  7480  nfoprab3  7481  zfcndrep  10692  zfcndpow  10694  zfcndreg  10695  zfcndinf  10696  reclem2pr  11126  ex-natded9.26  31013  brabgaf  33193  bnj607  35539  bnj849  35548  bnj1398  35657  bnj1449  35671  finminlem  37086  exisym1  37192  bj-alexbiex  37581  bj-exexbiex  37582  bj-biexal2  37588  bj-biexex  37591  bj-sbf3  37731  bj-axseprep  37970  bj-axreprepsep  37971  copsex2d  38040  sbexi  39025  ac6s6  39084  nfe2  43247  e2ebind  45531  e2ebindVD  45879  e2ebindALT  45896  stoweidlem57  47036  ovncvrrp  47543  ich2ex  48519  ichreuopeq  48524  reuopreuprim  48577  pgind  50779