Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  df-ceihi

Definition df-ceihi 267
Description: The predicate which is always true. Note that both sides are relational: the left-hand side definitionally only has one inhabitant, so this definition asserts that {ko'a du ko'a} is only true via one path. For related statements which reinforce this idea, see ceihi 268 or ceihi-nf 443.
Assertion
Ref Expression
df-ceihigo cei'i gi ko'a du ko'a

This definition is referenced by:  ceihi  268
  Copyright terms: Public domain W3C validator