Theorem hbe1 1495

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

Syntax hints:   → wi 4  ∀wal 1351  ∃wex 1492

This theorem was proved from axioms:  ax-ie1 1493

This theorem is referenced by:  nfe1  1496  19.8a  1590  exim  1599  19.43  1628  hbex  1636  excomim  1663  19.38  1676  exan  1693  equs5e  1795  exdistrfor  1800  hbmo1  2064  euan  2082  euor2  2084  eupicka  2106  mopick2  2109  moexexdc  2110  2moex  2112  2euex  2113  2exeu  2118  2eu4  2119  2eu7  2120