Theorem hbe1 1543

Description: 𝑥 is not free in ∃𝑥𝜑. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
hbe1	⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)

Proof of Theorem hbe1

Step	Hyp	Ref	Expression
1		ax-ie1 1541	1 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1395  ∃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  1710  19.38  1723  exan  1740  equs5e  1842  exdistrfor  1847  hbmo1  2116  euan  2135  euor2  2137  eupicka  2159  mopick2  2162  moexexdc  2163  2moex  2165  2euex  2166  2exeu  2171  2eu4  2172  2eu7  2173