Theorem nfe1 2161

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

Syntax hints:  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfa1  2162  nfnf1  2165  sbalex  2254  nf6  2294  exdistrf  2455  nfeu1  2593  euor2  2617  2moexv  2631  moexexvw  2632  2moswapv  2633  2euexv  2635  eupicka  2638  mopick2  2641  moexex  2642  2moex  2644  2euex  2645  2moswap  2648  2mo  2652  2eu7  2661  2eu8  2662  nfre1  3264  ceqsexg  3591  morex  3660  intab  4908  nfopab1  5142  nfopab2  5143  axrep1  5200  axrep2  5202  axrep3  5203  axrep4OLD  5206  eusv2nf  5324  copsexgwOLD  5431  copsexg  5432  copsex2t  5433  mosubopt  5451  dfid3  5516  dmcossOLD  5918  imadif  6569  oprabidw  7387  nfoprab1  7417  nfoprab2  7418  nfoprab3  7419  zfcndrep  10528  zfcndpow  10530  zfcndreg  10531  zfcndinf  10532  reclem2pr  10962  ex-natded9.26  30507  brabgaf  32698  bnj607  35098  bnj849  35107  bnj1398  35216  bnj1449  35230  finminlem  36546  exisym1  36652  bj-alexbiex  37042  bj-exexbiex  37043  bj-biexal2  37049  bj-biexex  37052  bj-sbf3  37192  bj-axseprep  37427  bj-axreprepsep  37428  copsex2d  37499  sbexi  38480  ac6s6  38539  nfe2  42700  e2ebind  45007  e2ebindVD  45355  e2ebindALT  45372  stoweidlem57  46500  ovncvrrp  47007  ich2ex  47943  ichreuopeq  47948  reuopreuprim  48001  pgind  50207