Theorem nfe1 2147

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

Syntax hints:  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfa1  2148  nfnf1  2151  nf6  2280  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  3239  ceqsexg  3583  morex  3654  intab  4909  nfopab1  5144  nfopab2  5145  axrep1  5210  axrep2  5212  axrep3  5213  axrep4  5214  eusv2nf  5318  copsexgw  5404  copsexg  5405  copsex2t  5406  copsex2gOLD  5408  mosubopt  5424  dfid3  5492  dmcoss  5880  imadif  6518  oprabidw  7306  nfoprab1  7336  nfoprab2  7337  nfoprab3  7338  fsplitOLD  7958  zfcndrep  10370  zfcndpow  10372  zfcndreg  10373  zfcndinf  10374  reclem2pr  10804  ex-natded9.26  28783  brabgaf  30948  bnj607  32896  bnj849  32905  bnj1398  33014  bnj1449  33028  finminlem  34507  exisym1  34613  bj-alexbiex  34881  bj-exexbiex  34882  bj-biexal2  34888  bj-biexex  34891  bj-sbf3  35022  copsex2d  35310  sbexi  36271  ac6s6  36330  e2ebind  42183  e2ebindVD  42532  e2ebindALT  42549  stoweidlem57  43598  ovncvrrp  44102  ich2ex  44920  ichreuopeq  44925  reuopreuprim  44978