Theorem hbe1 1452

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

Syntax hints:   → wi 4  ∀wal 1310  ∃wex 1449

This theorem was proved from axioms:  ax-ie1 1450

This theorem is referenced by:  nfe1  1453  19.8a  1550  exim  1559  19.43  1588  hbex  1596  excomim  1622  19.38  1635  exan  1652  equs5e  1747  exdistrfor  1752  hbmo1  2011  euan  2029  euor2  2031  eupicka  2053  mopick2  2056  moexexdc  2057  2moex  2059  2euex  2060  2exeu  2065  2eu4  2066  2eu7  2067