Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj14 Unicode version

Definition df-bnj14 28714
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
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cX . . 3  class  X
41, 2, 3c-bnj14 28713 . 2  class  pred ( X ,  A ,  R )
5 vy . . . . 5  set  y
65cv 1622 . . . 4  class  y
76, 3, 2wbr 4023 . . 3  wff  y R X
87, 5, 1crab 2547 . 2  class  { y  e.  A  |  y R X }
94, 8wceq 1623 1  wff  pred ( X ,  A ,  R )  =  {
y  e.  A  | 
y R X }
Colors of variables: wff set class
This definition is referenced by:  bnj213  28914  bnj602  28947  bnj1152  29028  bnj1279  29048  bnj1418  29070
  Copyright terms: Public domain W3C validator