ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hbe1 GIF version

Theorem hbe1 1456
Description: 𝑥 is not free in 𝑥𝜑. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbe1 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1454 1 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wex 1453
This theorem was proved from axioms:  ax-ie1 1454
This theorem is referenced by:  nfe1  1457  19.8a  1554  exim  1563  19.43  1592  hbex  1600  excomim  1626  19.38  1639  exan  1656  equs5e  1751  exdistrfor  1756  hbmo1  2015  euan  2033  euor2  2035  eupicka  2057  mopick2  2060  moexexdc  2061  2moex  2063  2euex  2064  2exeu  2069  2eu4  2070  2eu7  2071
  Copyright terms: Public domain W3C validator