Metamath Proof Explorer
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 |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cB |
|
1 |
|
cA |
|
2 |
|
cR |
|
3 |
1 0 2
|
w-bnj19 |
|
4 |
|
vx |
|
5 |
4
|
cv |
|
6 |
1 2 5
|
c-bnj14 |
|
7 |
6 0
|
wss |
|
8 |
7 4 0
|
wral |
|
9 |
3 8
|
wb |
|