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  2670  ceqsexg  2970  morex  3020  sbc6g  3071  intab  3956  copsexg  4607  copsex2t  4608  copsex2g  4609  mosubopt  4612  nfopab1  4628  nfopab2  4629  dfid3  4768  imadif  5171  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548