Theorem nfe1 2149

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

Syntax hints:  ∃wex 1783  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfa1  2150  nfnf1  2153  nf6  2283  exdistrf  2447  nfeu1ALT  2589  euor2  2615  2moexv  2629  moexexvw  2630  2moswapv  2631  2euexv  2633  eupicka  2636  mopick2  2639  moexex  2640  2moex  2642  2euex  2643  2moswap  2646  2mo  2650  2eu7  2659  2eu8  2660  nfre1  3234  ceqsexg  3575  morex  3649  intab  4906  nfopab1  5140  nfopab2  5141  axrep1  5206  axrep2  5208  axrep3  5209  axrep4  5210  eusv2nf  5313  copsexgw  5398  copsexg  5399  copsex2t  5400  copsex2gOLD  5402  mosubopt  5418  dfid3  5483  dmcoss  5869  imadif  6502  oprabidw  7286  nfoprab1  7314  nfoprab2  7315  nfoprab3  7316  fsplitOLD  7929  zfcndrep  10301  zfcndpow  10303  zfcndreg  10304  zfcndinf  10305  reclem2pr  10735  ex-natded9.26  28684  brabgaf  30849  bnj607  32796  bnj849  32805  bnj1398  32914  bnj1449  32928  finminlem  34434  exisym1  34540  bj-alexbiex  34808  bj-exexbiex  34809  bj-biexal2  34815  bj-biexex  34818  bj-sbf3  34949  copsex2d  35237  sbexi  36198  ac6s6  36257  e2ebind  42072  e2ebindVD  42421  e2ebindALT  42438  stoweidlem57  43488  ovncvrrp  43992  ich2ex  44808  ichreuopeq  44813  reuopreuprim  44866