Theorem nfe1 2027

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

Syntax hints:  ∃wex 1704  Ⅎwnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfa1  2028  nfnf1  2031  nf6  2117  exdistrf  2333  nfmo1  2481  euor2  2514  eupicka  2537  mopick2  2540  moexex  2541  2moex  2543  2euex  2544  2moswap  2547  2mo  2551  2eu7  2559  2eu8  2560  nfre1  3005  ceqsexg  3334  morex  3390  intab  4507  nfopab1  4719  nfopab2  4720  axrep1  4772  axrep2  4773  axrep3  4774  axrep4  4775  eusv2nf  4864  copsexg  4956  copsex2t  4957  copsex2g  4958  mosubopt  4972  dfid3  5025  dmcoss  5385  imadif  5973  nfoprab1  6704  nfoprab2  6705  nfoprab3  6706  fsplit  7282  zfcndrep  9436  zfcndpow  9438  zfcndreg  9439  zfcndinf  9440  reclem2pr  9870  ex-natded9.26  27276  brabgaf  29420  bnj607  30986  bnj849  30995  bnj1398  31102  bnj1449  31116  finminlem  32312  exisym1  32423  bj-alexbiex  32690  bj-exexbiex  32691  bj-biexal2  32697  bj-biexex  32700  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  bj-sbf3  32826  sbexi  33916  ac6s6  33980  e2ebind  38779  e2ebindVD  39148  e2ebindALT  39165  stoweidlem57  40274  ovncvrrp  40778