Definition df-bnj19 30763

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4	1, 2, 3	w-bnj19 30762	. 2 wff TrFo ( B , A , R )
5		vx	. . . . . 6 setvar x
6	5	cv 1482	. . . . 5 class x
7	1, 3, 6	c-bnj14 30754	. . . 4 class pred ( x , A , R )
8	7, 2	wss 3574	. . 3 wff pred ( x , A , R ) C_ B
9	8, 5, 2	wral 2912	. 2 wff A. x e. B pred ( x , A , R ) C_ B
10	4, 9	wb 196	1 wff ( TrFo ( B , A , R ) <-> A. x e. B pred ( x , A , R ) C_ B )

This definition is referenced by:  bnj978  31019  bnj1118  31052  bnj1125  31060  bnj1137  31063  bnj1408  31104