Metamath Proof Explorer


Definition df-bnj19

Description: Define the following predicate: B is transitive for A and R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion df-bnj19
|- ( _TrFo ( B , A , R ) <-> A. x e. B _pred ( x , A , R ) C_ B )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cB
 |-  B
1 cA
 |-  A
2 cR
 |-  R
3 1 0 2 w-bnj19
 |-  _TrFo ( B , A , R )
4 vx
 |-  x
5 4 cv
 |-  x
6 1 2 5 c-bnj14
 |-  _pred ( x , A , R )
7 6 0 wss
 |-  _pred ( x , A , R ) C_ B
8 7 4 0 wral
 |-  A. x e. B _pred ( x , A , R ) C_ B
9 3 8 wb
 |-  ( _TrFo ( B , A , R ) <-> A. x e. B _pred ( x , A , R ) C_ B )