Theorem hbe1 1518

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

Syntax hints:   -> wi 4   A.wal 1371   E.wex 1515

This theorem was proved from axioms:  ax-ie1 1516

This theorem is referenced by:  nfe1  1519  19.8a  1613  exim  1622  19.43  1651  hbex  1659  excomim  1686  19.38  1699  exan  1716  equs5e  1818  exdistrfor  1823  hbmo1  2092  euan  2110  euor2  2112  eupicka  2134  mopick2  2137  moexexdc  2138  2moex  2140  2euex  2141  2exeu  2146  2eu4  2147  2eu7  2148