brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  brdpu

---

Syntax Definition brdpu 381

Description: Restriction for first-order identity.

Hypotheses

Ref	Expression
wk1	sumti ko'a
sbb1	bridi broda
wda	sumti da
brdpu.0	bridi ro da zo'u broda

Assertion

Ref	Expression
brdpu	bridi ro da po'u ko'a zo'u broda

---

See definition df-pohu 382 for more information.

---

Colors of variables: sumti selbri bridi

Copyright terms: Public domain

W3C validator