Theorem hbe1 1424

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

Syntax hints:   → wi 4  ∀wal 1282  ∃wex 1421

This theorem was proved from axioms:  ax-ie1 1422

This theorem is referenced by:  nfe1  1425  19.8a  1522  exim  1530  19.43  1559  hbex  1567  excomim  1593  19.38  1606  exan  1623  equs5e  1716  exdistrfor  1721  hbmo1  1979  euan  1997  euor2  1999  eupicka  2021  mopick2  2024  moexexdc  2025  2moex  2027  2euex  2028  2exeu  2033  2eu4  2034  2eu7  2035