Theorem hbe1 1471

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

Syntax hints:   -> wi 4   A.wal 1329   E.wex 1468

This theorem was proved from axioms:  ax-ie1 1469

This theorem is referenced by:  nfe1  1472  19.8a  1569  exim  1578  19.43  1607  hbex  1615  excomim  1641  19.38  1654  exan  1671  equs5e  1767  exdistrfor  1772  hbmo1  2035  euan  2053  euor2  2055  eupicka  2077  mopick2  2080  moexexdc  2081  2moex  2083  2euex  2084  2exeu  2089  2eu4  2090  2eu7  2091