Definition df-bnj14 30755

Description: Define the function giving: the class of all elements of A that are "smaller" than X according to R. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bnj14	|- pred ( X , A , R ) = { y e. A | y R X }

Distinct variable groups:   y, X   y, A   y, R

Detailed syntax breakdown of Definition df-bnj14

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cX	. . 3 class X
4	1, 2, 3	c-bnj14 30754	. 2 class pred ( X , A , R )
5		vy	. . . . 5 setvar y
6	5	cv 1482	. . . 4 class y
7	6, 3, 2	wbr 4653	. . 3 wff y R X
8	7, 5, 1	crab 2916	. 2 class { y e. A | y R X }
9	4, 8	wceq 1483	1 wff pred ( X , A , R ) = { y e. A | y R X }

This definition is referenced by:  bnj213  30952  bnj602  30985  bnj1152  31066  bnj1279  31086  bnj1418  31108