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