Theorem nfe1 2174

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

Syntax hints:  ∃wex 1789  Ⅎwnf 1793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-10 2165

This theorem depends on definitions:  df-bi 209  df-ex 1790  df-nf 1794

This theorem is referenced by:  nfa1  2175  nfnf1  2178  sbalex  2267  nf6  2307  exdistrf  2468  nfeu1  2606  euor2  2630  2moexv  2644  moexexvw  2645  2moswapv  2646  2euexv  2648  eupicka  2651  mopick2  2654  moexex  2655  2moex  2657  2euex  2658  2moswap  2661  2mo  2665  2eu7  2674  2eu8  2675  nfre1  3277  ceqsexg  3603  morex  3672  intab  4926  nfopab1  5160  nfopab2  5161  axrep1  5218  axrep2  5220  axrep3  5221  axrep4OLD  5224  eusv2nf  5342  copsexgwOLD  5449  copsexg  5450  copsex2t  5451  mosubopt  5469  dfid3  5534  dmcossOLD  5941  imadif  6590  oprabidw  7412  nfoprab1  7442  nfoprab2  7443  nfoprab3  7444  zfcndrep  10558  zfcndpow  10560  zfcndreg  10561  zfcndinf  10562  reclem2pr  10992  ex-natded9.26  30556  brabgaf  32747  bnj607  35158  bnj849  35167  bnj1398  35276  bnj1449  35290  finminlem  36616  exisym1  36722  bj-alexbiex  37112  bj-exexbiex  37113  bj-biexal2  37119  bj-biexex  37122  bj-sbf3  37262  bj-axseprep  37497  bj-axreprepsep  37498  copsex2d  37569  sbexi  38550  ac6s6  38609  nfe2  42770  e2ebind  45077  e2ebindVD  45425  e2ebindALT  45442  stoweidlem57  46569  ovncvrrp  47076  ich2ex  48012  ichreuopeq  48017  reuopreuprim  48070  pgind  50276