Theorem nfe1 2150

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

Syntax hints:  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfa1  2151  nfnf1  2154  sbalex  2242  nf6  2283  exdistrf  2451  nfeu1ALT  2588  euor2  2612  2moexv  2626  moexexvw  2627  2moswapv  2628  2euexv  2630  eupicka  2633  mopick2  2636  moexex  2637  2moex  2639  2euex  2640  2moswap  2643  2mo  2647  2eu7  2657  2eu8  2658  nfre1  3267  ceqsexg  3632  morex  3702  intab  4954  nfopab1  5189  nfopab2  5190  axrep1  5250  axrep2  5252  axrep3  5253  axrep4OLD  5256  eusv2nf  5365  copsexgw  5465  copsexg  5466  copsex2t  5467  mosubopt  5485  dfid3  5551  dmcoss  5954  imadif  6619  oprabidw  7434  nfoprab1  7466  nfoprab2  7467  nfoprab3  7468  zfcndrep  10626  zfcndpow  10628  zfcndreg  10629  zfcndinf  10630  reclem2pr  11060  ex-natded9.26  30346  brabgaf  32534  bnj607  34893  bnj849  34902  bnj1398  35011  bnj1449  35025  finminlem  36282  exisym1  36388  bj-alexbiex  36663  bj-exexbiex  36664  bj-biexal2  36670  bj-biexex  36673  bj-sbf3  36803  copsex2d  37103  sbexi  38083  ac6s6  38142  e2ebind  44536  e2ebindVD  44884  e2ebindALT  44901  stoweidlem57  46034  ovncvrrp  46541  ich2ex  47430  ichreuopeq  47435  reuopreuprim  47488  pgind  49529