Metamath Proof Explorer


Syntax definition cpred

Description: The predecessors symbol.

Ref Expression
Assertion cpred class Pred ( 𝑅 , 𝐴 , 𝑋 )