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

Definition df-bnj19 29038
Description: Define the following predicate:  B is transitive for  A and  R. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj19  |-  (  TrFo ( B ,  A ,  R )  <->  A. x  e.  B  pred ( x ,  A ,  R
)  C_  B )
Distinct variable groups:    x, B    x, A    x, R

Detailed syntax breakdown of Definition df-bnj19
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
41, 2, 3w-bnj19 29037 . 2  wff  TrFo ( B ,  A ,  R )
5 vx . . . . . 6  set  x
65cv 1631 . . . . 5  class  x
71, 3, 6c-bnj14 29029 . . . 4  class  pred (
x ,  A ,  R )
87, 2wss 3165 . . 3  wff  pred (
x ,  A ,  R )  C_  B
98, 5, 2wral 2556 . 2  wff  A. x  e.  B  pred ( x ,  A ,  R
)  C_  B
104, 9wb 176 1  wff  (  TrFo ( B ,  A ,  R )  <->  A. x  e.  B  pred ( x ,  A ,  R
)  C_  B )
Colors of variables: wff set class
This definition is referenced by:  bnj978  29297  bnj1118  29330  bnj1125  29338  bnj1137  29341  bnj1408  29382
  Copyright terms: Public domain W3C validator