Definition df-bnj13 30757

Description: Define the following predicate: R is set-like on A. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bnj13	|- ( R Se A <-> A. x e. A pred ( x , A , R ) e. _V )

Distinct variable groups:   x, R   x, A

Detailed syntax breakdown of Definition df-bnj13

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	w-bnj13 30756	. 2 wff R Se A
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6	1, 2, 5	c-bnj14 30754	. . . 4 class pred ( x , A , R )
7		cvv 3200	. . . 4 class _V
8	6, 7	wcel 1990	. . 3 wff pred ( x , A , R ) e. _V
9	8, 4, 1	wral 2912	. 2 wff A. x e. A pred ( x , A , R ) e. _V
10	3, 9	wb 196	1 wff ( R Se A <-> A. x e. A pred ( x , A , R ) e. _V )

This definition is referenced by:  bnj93  30933  bnj1489  31124