Theorem nfe1 1732

Description: x is not free in ∃xφ. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfe1	⊢ Ⅎx∃xφ

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 1731	. 2 ⊢ (∃xφ → ∀x∃xφ)
2	1	nfi 1551	1 ⊢ Ⅎx∃xφ

Syntax hints:  ∃wex 1541  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-6 1729

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.23tOLD  1819  excomimOLD  1858  nf3  1867  19.38OLD  1874  exan  1882  equs5e  1888  exdistrf  1971  nfmo1  2215  euan  2261  eupicka  2268  mopick2  2271  euor2  2272  moexex  2273  2moex  2275  2euex  2276  2moswap  2279  2eu4  2287  2eu7  2290  2eu8  2291  nfre1  2671  ceqsexg  2971  morex  3021  sbc6g  3072  intab  3957  copsexg  4608  copsex2t  4609  copsex2g  4610  mosubopt  4613  nfopab1  4629  nfopab2  4630  dfid3  4769  imadif  5172  nfoprab1  5547  nfoprab2  5548  nfoprab3  5549