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 x B pred x A R B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cB class B
1 cA class A
2 cR class R
3 1 0 2 w-bnj19 wff TrFo B A R
4 vx setvar x
5 4 cv setvar x
6 1 2 5 c-bnj14 class pred x A R
7 6 0 wss wff pred x A R B
8 7 4 0 wral wff x B pred x A R B
9 3 8 wb wff TrFo B A R x B pred x A R B