Theorem hbe1 1506

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

Syntax hints:   → wi 4  ∀wal 1362  ∃wex 1503

This theorem was proved from axioms:  ax-ie1 1504

This theorem is referenced by:  nfe1  1507  19.8a  1601  exim  1610  19.43  1639  hbex  1647  excomim  1674  19.38  1687  exan  1704  equs5e  1806  exdistrfor  1811  hbmo1  2080  euan  2098  euor2  2100  eupicka  2122  mopick2  2125  moexexdc  2126  2moex  2128  2euex  2129  2exeu  2134  2eu4  2135  2eu7  2136