Theorem nfe1 2186

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

This proof depends on syntax axioms:  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2177

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfa1  2187  nfnf1  2190  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  3606  morex  3676  intab  4937  nfopab1  5174  nfopab2  5175  axrep1  5232  axrep2  5234  axrep3  5235  eusv2nf  5357  copsexgwOLD  5461  copsexg  5462  copsex2t  5464  mosubopt  5482  mosubott  5484  dfid3  5549  dmcossOLD  5959  imadif  6629  oprabidw  7455  nfoprab1  7485  nfoprab2  7486  nfoprab3  7487  zfcndrep  10706  zfcndpow  10708  zfcndreg  10709  zfcndinf  10710  reclem2pr  11140  ex-natded9.26  31029  brabgaf  33251  bnj607  35596  bnj849  35605  bnj1398  35714  bnj1449  35728  finminlem  37202  exisym1  37308  bj-alexbiex  37697  bj-exexbiex  37698  bj-biexal2  37704  bj-biexex  37707  bj-sbf3  37847  bj-axseprep  38098  bj-axreprepsep  38099  copsex2d  38169  sbexi  39154  ac6s6  39213  nfe2  43376  e2ebind  45654  e2ebindVD  46002  e2ebindALT  46019  stoweidlem57  47175  ovncvrrp  47682  ich2ex  48658  ichreuopeq  48663  reuopreuprim  48716  pgind  50993