NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  hbn1 Unicode version

Theorem hbn1 1730
Description: is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
Assertion
Ref Expression
hbn1

Proof of Theorem hbn1
StepHypRef Expression
1 ax-6 1729 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4  wal 1540
This theorem was proved from axioms:  ax-6 1729
This theorem is referenced by:  hbe1  1731  modal-5  1733  ax5o  1749  hbnOLD  1777  hba1OLD  1787  hbimdOLD  1816  dvelimhw  1849  ax12olem6  1932  dvelimv  1939  a16g  1945  ax15  2021  dvelimALT  2133  ax11indn  2195
  Copyright terms: Public domain W3C validator