Definition df-bnj14

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.)

	Ref	Expression
Assertion	df-bnj14	$$⊢pred\left(X,A,R\right)=\left\{y\in A|yRX\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cX	$$classX$$
1		cA	$$classA$$
2		cR	$$classR$$
3	1 2 0	c-bnj14	$$classpred\left(X,A,R\right)$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 0 2	wbr	$$wffyRX$$
7	6 4 1	crab	$$class\left\{y\in A|yRX\right\}$$
8	3 7	wceq	$$wffpred\left(X,A,R\right)=\left\{y\in A|yRX\right\}$$