This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer


Syntax definition c-bnj14

Description: Extend class notation with the function giving: the class of all elements of A that are "smaller" than X according to R . (New usage is discouraged.)

Ref Expression
Assertion c-bnj14 class pred X A R