df-je - brismu bridi

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

Definition df-je 119

Description: Definition of {je} in terms of {ge}. From example 12.2-5 of [CLL] p. 14.

**Assertion**
Ref	Expression
df-je	⊢ go ko'a bu'a je bu'e ko'e gi ge ko'a bu'a ko'e gi ko'a bu'e ko'e

Distinct variable group: bu'a ,bu'e

This definition is referenced by: jei 120 jeri 121