Theorem hbe1 1471

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

Syntax hints:   → wi 4  ∀wal 1329  ∃wex 1468

This theorem was proved from axioms:  ax-ie1 1469

This theorem is referenced by:  nfe1  1472  19.8a  1569  exim  1578  19.43  1607  hbex  1615  excomim  1641  19.38  1654  exan  1671  equs5e  1767  exdistrfor  1772  hbmo1  2037  euan  2055  euor2  2057  eupicka  2079  mopick2  2082  moexexdc  2083  2moex  2085  2euex  2086  2exeu  2091  2eu4  2092  2eu7  2093