Theorem hbe1 1548

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

Syntax hints:   -> wi 4   A.wal 1400   E.wex 1545

This theorem was proved from axioms:  ax-ie1 1546

This theorem is referenced by:  nfe1  1549  19.8a  1643  exim  1652  19.43  1681  hbex  1689  excomim  1715  19.38  1728  exan  1745  equs5e  1848  exdistrfor  1853  hbmo1  2124  euan  2143  euor2  2145  eupicka  2167  mopick2  2170  moexexdc  2171  2moex  2173  2euex  2174  2exeu  2179  2eu4  2180  2eu7  2181