Theorem hbe1 1384

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

Syntax hints:   -> wi 4   A.wal 1241   E.wex 1381

This theorem was proved from axioms:  ax-ie1 1382

This theorem is referenced by:  nfe1  1385  19.8a  1482  exim  1490  19.43  1519  hbex  1527  excomim  1553  19.38  1566  exan  1583  equs5e  1676  exdistrfor  1681  hbmo1  1938  euan  1956  euor2  1958  eupicka  1980  mopick2  1983  moexexdc  1984  2moex  1986  2euex  1987  2exeu  1992  2eu4  1993  2eu7  1994