Theorem hbe1 1541

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

Syntax hints:   → wi 4  ∀wal 1393  ∃wex 1538

This theorem was proved from axioms:  ax-ie1 1539

This theorem is referenced by:  nfe1  1542  19.8a  1636  exim  1645  19.43  1674  hbex  1682  excomim  1709  19.38  1722  exan  1739  equs5e  1841  exdistrfor  1846  hbmo1  2115  euan  2134  euor2  2136  eupicka  2158  mopick2  2161  moexexdc  2162  2moex  2164  2euex  2165  2exeu  2170  2eu4  2171  2eu7  2172