Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  bsub
Syntax Definition bsub 446
Description: Metasyntax for substitutions. In this example, we are replacing every instance of {da} within {broda} with {ko'a}.
Hypotheses
Ref Expression
wk1 sumti ko'a
sbb1 bridi broda
wda sumti da
Assertion
Ref Expression
bsub bridi [ ko'a / da ] broda
See definition df-sub 447 for more information.
Colors of variables: sumti selbri bridi
  Copyright terms: Public domain W3C validator