Theorem hbe1 1454

Description: x is not free in E. x ph. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
hbe1	|- ( E. x ph -> A. x E. x ph )

Proof of Theorem hbe1

Step	Hyp	Ref	Expression
1		ax-ie1 1452	1 |- ( E. x ph -> A. x E. x ph )

Syntax hints:   -> wi 4   A.wal 1312   E.wex 1451

This theorem was proved from axioms:  ax-ie1 1452

This theorem is referenced by:  nfe1  1455  19.8a  1552  exim  1561  19.43  1590  hbex  1598  excomim  1624  19.38  1637  exan  1654  equs5e  1749  exdistrfor  1754  hbmo1  2013  euan  2031  euor2  2033  eupicka  2055  mopick2  2058  moexexdc  2059  2moex  2061  2euex  2062  2exeu  2067  2eu4  2068  2eu7  2069