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

Syntax Definition brdp 370
Description: Restriction for first-order universal quantification.
Hypotheses
Ref Expression
sbb1 bridi broda
tb1 brirebla bo'a
wda sumti da
brdp.0 bridi ro da zo'u broda
Assertion
Ref Expression
brdp bridi ro da poi ke'a bo'a ku'o zo'u broda

See definition df-poi-ro 372 for more information.

Colors of variables: sumti selbri bridi
  Copyright terms: Public domain W3C validator