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

---

Syntax Definition bsdp 371

Description: Restriction for first-order universal quantification.

Hypotheses

Ref	Expression
sbb1	bridi broda
tb1	brirebla bo'a
wda	sumti da
bsdp.0	bridi su'o da zo'u broda

Assertion

Ref	Expression
bsdp	bridi su'o da poi ke'a bo'a ku'o zo'u broda

---

This syntax is primitive. The first axiom using it is ax-nat-ind 490.

---

Colors of variables: sumti selbri bridi

Copyright terms: Public domain

W3C validator