c-bnj14 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > c-bnj14		Structured version Visualization version GIF version

Syntax Definition c-bnj14 31953

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

**Hypotheses**
Ref	Expression
cA	class 𝐴
cR	class 𝑅
cX	class 𝑋

**Assertion**
Ref	Expression
c-bnj14	class pred(𝑋, 𝐴, 𝑅)

See definition df-bnj14 31954 for more information.

Colors of variables: wff setvar class

W3C validator