Theorem nfe1 2140

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

Syntax hints:  ∃wex 1774  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfa1  2141  nfnf1  2144  nf6  2273  exdistrf  2442  nfeu1ALT  2579  euor2  2605  2moexv  2619  moexexvw  2620  2moswapv  2621  2euexv  2623  eupicka  2626  mopick2  2629  moexex  2630  2moex  2632  2euex  2633  2moswap  2636  2mo  2640  2eu7  2649  2eu8  2650  nfre1  3278  ceqsexg  3638  morex  3713  intab  4977  nfopab1  5213  nfopab2  5214  axrep1  5281  axrep2  5283  axrep3  5284  axrep4  5285  eusv2nf  5390  copsexgw  5487  copsexg  5488  copsex2t  5489  copsex2gOLD  5491  mosubopt  5507  dfid3  5574  dmcoss  5969  imadif  6632  oprabidw  7446  nfoprab1  7476  nfoprab2  7477  nfoprab3  7478  zfcndrep  10632  zfcndpow  10634  zfcndreg  10635  zfcndinf  10636  reclem2pr  11066  ex-natded9.26  30223  brabgaf  32392  bnj607  34542  bnj849  34551  bnj1398  34660  bnj1449  34674  finminlem  35797  exisym1  35903  bj-alexbiex  36171  bj-exexbiex  36172  bj-biexal2  36178  bj-biexex  36181  bj-sbf3  36311  copsex2d  36613  sbexi  37581  ac6s6  37640  e2ebind  43993  e2ebindVD  44342  e2ebindALT  44359  stoweidlem57  45436  ovncvrrp  45943  ich2ex  46799  ichreuopeq  46804  reuopreuprim  46857  pgind  48139