Theorem nfe1 2184

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

Syntax hints:  ∃wex 1799  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-10 2175

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfa1  2185  nfnf1  2188  sbalex  2277  nf6  2317  exdistrf  2478  nfeu1  2616  euor2  2640  2moexv  2654  moexexvw  2655  2moswapv  2656  2euexv  2658  eupicka  2661  mopick2  2664  moexex  2665  2moex  2667  2euex  2668  2moswap  2671  2mo  2675  2eu7  2684  2eu8  2685  nfre1  3287  ceqsexg  3612  morex  3682  intab  4936  nfopab1  5170  nfopab2  5171  axrep1  5228  axrep2  5230  axrep3  5231  axrep4OLD  5234  eusv2nf  5352  copsexgwOLD  5459  copsexg  5460  copsex2t  5461  mosubopt  5479  dfid3  5545  dmcossOLD  5952  imadif  6605  oprabidw  7427  nfoprab1  7457  nfoprab2  7458  nfoprab3  7459  zfcndrep  10572  zfcndpow  10574  zfcndreg  10575  zfcndinf  10576  reclem2pr  11006  ex-natded9.26  30618  brabgaf  32805  bnj607  35208  bnj849  35217  bnj1398  35326  bnj1449  35340  finminlem  36675  exisym1  36781  bj-alexbiex  37171  bj-exexbiex  37172  bj-biexal2  37178  bj-biexex  37181  bj-sbf3  37321  bj-axseprep  37556  bj-axreprepsep  37557  copsex2d  37628  sbexi  38609  ac6s6  38668  nfe2  42829  e2ebind  45136  e2ebindVD  45484  e2ebindALT  45501  stoweidlem57  46628  ovncvrrp  47135  ich2ex  48071  ichreuopeq  48076  reuopreuprim  48129  pgind  50335