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 2144	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2147	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 2142

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

This theorem is referenced by:  nfa1  2152  nfnf1  2155  sbalex  2243  nf6  2283  exdistrf  2446  nfeu1ALT  2583  euor2  2607  2moexv  2621  moexexvw  2622  2moswapv  2623  2euexv  2625  eupicka  2628  mopick2  2631  moexex  2632  2moex  2634  2euex  2635  2moswap  2638  2mo  2642  2eu7  2652  2eu8  2653  nfre1  3263  ceqsexg  3622  morex  3693  intab  4945  nfopab1  5180  nfopab2  5181  axrep1  5238  axrep2  5240  axrep3  5241  axrep4OLD  5244  eusv2nf  5353  copsexgw  5453  copsexg  5454  copsex2t  5455  mosubopt  5473  dfid3  5539  dmcoss  5941  imadif  6603  oprabidw  7421  nfoprab1  7453  nfoprab2  7454  nfoprab3  7455  zfcndrep  10574  zfcndpow  10576  zfcndreg  10577  zfcndinf  10578  reclem2pr  11008  ex-natded9.26  30355  brabgaf  32543  bnj607  34913  bnj849  34922  bnj1398  35031  bnj1449  35045  finminlem  36313  exisym1  36419  bj-alexbiex  36694  bj-exexbiex  36695  bj-biexal2  36701  bj-biexex  36704  bj-sbf3  36834  copsex2d  37134  sbexi  38114  ac6s6  38173  e2ebind  44560  e2ebindVD  44908  e2ebindALT  44925  stoweidlem57  46062  ovncvrrp  46569  ich2ex  47473  ichreuopeq  47478  reuopreuprim  47531  pgind  49710