Theorem hbe1 1488

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

Syntax hints:   → wi 4  ∀wal 1346  ∃wex 1485

This theorem was proved from axioms:  ax-ie1 1486

This theorem is referenced by:  nfe1  1489  19.8a  1583  exim  1592  19.43  1621  hbex  1629  excomim  1656  19.38  1669  exan  1686  equs5e  1788  exdistrfor  1793  hbmo1  2057  euan  2075  euor2  2077  eupicka  2099  mopick2  2102  moexexdc  2103  2moex  2105  2euex  2106  2exeu  2111  2eu4  2112  2eu7  2113