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  2118  euan  2137  euor2  2139  eupicka  2161  mopick2  2164  moexexdc  2165  2moex  2167  2euex  2168  2exeu  2173  2eu4  2174  2eu7  2175