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

---

Definition df-simxu 393

Description: An alternate definition of {simxu} which doesn't use {poi ke'a cmima} for element selection.

Assertion

Ref	Expression
df-simxu	⊢ go ko'a simxu ko'e gi ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e

Distinct variable group:   da , de

---

This definition is referenced by:  simxui  394  simxuri  395

Copyright terms: Public domain

W3C validator