Theorem hbe1 1519

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

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

This theorem was proved from axioms:  ax-ie1 1517

This theorem is referenced by:  nfe1  1520  19.8a  1614  exim  1623  19.43  1652  hbex  1660  excomim  1687  19.38  1700  exan  1717  equs5e  1819  exdistrfor  1824  hbmo1  2093  euan  2112  euor2  2114  eupicka  2136  mopick2  2139  moexexdc  2140  2moex  2142  2euex  2143  2exeu  2148  2eu4  2149  2eu7  2150