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

Metamath Proof Explorer

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 (X, A, R) = \{y \in A \| y R X\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cX	$class X$
1		cA	$class A$
2		cR	$class R$
3	1 2 0	c-bnj14	$class pred (X, A, R)$
4		vy	$setvar y$
5	4	cv	$setvar y$
6	5 0 2	wbr	$wff y R X$
7	6 4 1	crab	$class \{y \in A \| y R X\}$
8	3 7	wceq	$wff pred (X, A, R) = \{y \in A \| y R X\}$