Theorem hbe1 1519

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

Syntax hints:   → wi 4  ∀wal 1371  ∃wex 1516

This theorem was proved from axioms:  ax-ie1 1517

This theorem is referenced by:  nfe1  1520  19.8a  1614  exim  1623  19.43  1652  hbex  1660  excomim  1687  19.38  1700  exan  1717  equs5e  1819  exdistrfor  1824  hbmo1  2093  euan  2111  euor2  2113  eupicka  2135  mopick2  2138  moexexdc  2139  2moex  2141  2euex  2142  2exeu  2147  2eu4  2148  2eu7  2149