Theorem hbe1 1483

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

Syntax hints:   → wi 4  ∀wal 1341  ∃wex 1480

This theorem was proved from axioms:  ax-ie1 1481

This theorem is referenced by:  nfe1  1484  19.8a  1578  exim  1587  19.43  1616  hbex  1624  excomim  1651  19.38  1664  exan  1681  equs5e  1783  exdistrfor  1788  hbmo1  2052  euan  2070  euor2  2072  eupicka  2094  mopick2  2097  moexexdc  2098  2moex  2100  2euex  2101  2exeu  2106  2eu4  2107  2eu7  2108