Nearby theorems
|
|
brismu bridi |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > Home > Th. List > df-ceihi | |||
| 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 232 or ceihi-nf 404. |
| Ref | Expression |
|---|---|
| df-ceihi | ⊢ go cei'i gi ko'a du ko'a |
| Copyright terms: Public domain | W3C validator |