Metamath Proof Explorer


Syntax definition c-bnj18

Description: Extend class notation with the function giving: the transitive closure of X in A by R . (New usage is discouraged.)

Ref Expression
Assertion c-bnj18 class trCl ( 𝑋 , 𝐴 , 𝑅 )