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  1844  exdistrfor  1849  hbmo1  2120  euan  2139  euor2  2141  eupicka  2163  mopick2  2166  moexexdc  2167  2moex  2169  2euex  2170  2exeu  2175  2eu4  2176  2eu7  2177