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

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

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1398 1 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wex 1397
This theorem was proved from axioms:  ax-ie1 1398
This theorem is referenced by:  nfe1  1401  19.8a  1498  exim  1506  19.43  1535  hbex  1543  excomim  1569  19.38  1582  exan  1599  equs5e  1692  exdistrfor  1697  hbmo1  1954  euan  1972  euor2  1974  eupicka  1996  mopick2  1999  moexexdc  2000  2moex  2002  2euex  2003  2exeu  2008  2eu4  2009  2eu7  2010
  Copyright terms: Public domain W3C validator