Theorem nfe1 2151

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

Syntax hints:  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2142

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfa1  2152  nfnf1  2155  nf6  2287  exdistrf  2458  nfeu1ALT  2650  euor2  2674  2moexv  2689  moexexvw  2690  2moswapv  2691  2euexv  2693  eupicka  2696  mopick2  2699  moexex  2700  2moex  2702  2euex  2703  2moswap  2706  2mo  2710  2eu7  2720  2eu8  2721  nfre1  3265  ceqsexg  3594  morex  3658  intab  4868  nfopab1  5099  nfopab2  5100  axrep1  5155  axrep2  5157  axrep3  5158  axrep4  5159  eusv2nf  5261  copsexgw  5346  copsexg  5347  copsex2t  5348  copsex2g  5349  mosubopt  5365  dfid3  5427  dmcoss  5807  imadif  6408  oprabidw  7166  nfoprab1  7194  nfoprab2  7195  nfoprab3  7196  fsplitOLD  7796  zfcndrep  10025  zfcndpow  10027  zfcndreg  10028  zfcndinf  10029  reclem2pr  10459  ex-natded9.26  28204  brabgaf  30372  bnj607  32298  bnj849  32307  bnj1398  32416  bnj1449  32430  finminlem  33779  exisym1  33885  bj-alexbiex  34146  bj-exexbiex  34147  bj-biexal2  34153  bj-biexex  34156  bj-sbf3  34277  copsex2d  34554  sbexi  35551  ac6s6  35610  e2ebind  41269  e2ebindVD  41618  e2ebindALT  41635  stoweidlem57  42699  ovncvrrp  43203  ich2ex  43985  ichreuopeq  43990  reuopreuprim  44043