Theorem hbe1 1544

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 1542	1 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1396  ∃wex 1541

This theorem was proved from axioms:  ax-ie1 1542

This theorem is referenced by:  nfe1  1545  19.8a  1639  exim  1648  19.43  1677  hbex  1685  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