Theorem hbe1 1543

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

Syntax hints:   -> wi 4   A.wal 1395   E.wex 1540

This theorem was proved from axioms:  ax-ie1 1541

This theorem is referenced by:  nfe1  1544  19.8a  1638  exim  1647  19.43  1676  hbex  1684  excomim  1711  19.38  1724  exan  1741  equs5e  1843  exdistrfor  1848  hbmo1  2117  euan  2136  euor2  2138  eupicka  2160  mopick2  2163  moexexdc  2164  2moex  2166  2euex  2167  2exeu  2172  2eu4  2173  2eu7  2174