Metamath Proof Explorer


Syntax definition w-bnj19

Description: Extend wff notation with the following predicate: B is transitive for A and R . (New usage is discouraged.)

Ref Expression
Assertion w-bnj19
wff _TrFo ( B , A , R )