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

Theorem hbe1 1425
Description:  x is not free in  E. x ph. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbe1  |-  ( E. x ph  ->  A. x E. x ph )

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1423 1  |-  ( E. x ph  ->  A. x E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283   E.wex 1422
This theorem was proved from axioms:  ax-ie1 1423
This theorem is referenced by:  nfe1  1426  19.8a  1523  exim  1531  19.43  1560  hbex  1568  excomim  1594  19.38  1607  exan  1624  equs5e  1718  exdistrfor  1723  hbmo1  1981  euan  1999  euor2  2001  eupicka  2023  mopick2  2026  moexexdc  2027  2moex  2029  2euex  2030  2exeu  2035  2eu4  2036  2eu7  2037
  Copyright terms: Public domain W3C validator