Theorem hbe1 1475

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 1473	1 |- ( E. x ph -> A. x E. x ph )

Syntax hints:   -> wi 4   A.wal 1333   E.wex 1472

This theorem was proved from axioms:  ax-ie1 1473

This theorem is referenced by:  nfe1  1476  19.8a  1570  exim  1579  19.43  1608  hbex  1616  excomim  1643  19.38  1656  exan  1673  equs5e  1775  exdistrfor  1780  hbmo1  2044  euan  2062  euor2  2064  eupicka  2086  mopick2  2089  moexexdc  2090  2moex  2092  2euex  2093  2exeu  2098  2eu4  2099  2eu7  2100