Theorem hbe1 1509

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

Syntax hints:   -> wi 4   A.wal 1362   E.wex 1506

This theorem was proved from axioms:  ax-ie1 1507

This theorem is referenced by:  nfe1  1510  19.8a  1604  exim  1613  19.43  1642  hbex  1650  excomim  1677  19.38  1690  exan  1707  equs5e  1809  exdistrfor  1814  hbmo1  2083  euan  2101  euor2  2103  eupicka  2125  mopick2  2128  moexexdc  2129  2moex  2131  2euex  2132  2exeu  2137  2eu4  2138  2eu7  2139