Theorem nfe1 2190

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

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

This theorem is used by:  nfa1  2191  nfnf1  2194  sbalex  2282  nf6  2320  exdistrf  2479  nfeu1  2617  euor2  2641  2moexv  2655  moexexvw  2656  2moswapv  2657  2euexv  2659  eupicka  2662  mopick2  2665  moexex  2666  2moex  2668  2euex  2669  2moswap  2672  2mo  2676  2eu7  2685  2eu8  2686  nfre1  3291  ceqsexg  3610  morex  3680  intab  4943  nfopab1  5181  nfopab2  5182  axrep1  5239  axrep2  5241  axrep3  5242  eusv2nf  5364  copsexgwOLD  5468  copsexg  5469  copsex2t  5471  mosubopt  5489  mosubott  5491  dfid3  5556  dmcossOLD  5970  imadif  6654  oprabidw  7482  nfoprab1  7512  nfoprab2  7513  nfoprab3  7514  zfcndrep  10738  zfcndpow  10740  zfcndreg  10741  zfcndinf  10742  reclem2pr  11172  ex-natded9.26  31077  brabgaf  33298  bnj607  35657  bnj849  35666  bnj1398  35775  bnj1449  35789  finminlem  37321  exisym1  37427  bj-alexbiex  37816  bj-exexbiex  37817  bj-biexal2  37823  bj-biexex  37826  bj-sbf3  37966  bj-axseprep  38260  bj-axreprepsep  38261  copsex2d  38331  sbexi  39311  ac6s6  39370  nfe2  43534  e2ebind  45806  e2ebindVD  46154  e2ebindALT  46171  stoweidlem57  47340  ovncvrrp  47847  ich2ex  48823  ichreuopeq  48828  reuopreuprim  48881  pgind  51216