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 ( 𝐵 , 𝐴 , 𝑅 )