Definition df-bnj13 35378

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

Assertion

Ref	Expression
df-bnj13	⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V)

Distinct variable groups:   𝑥,𝑅   𝑥,𝐴

Detailed syntax breakdown of Definition df-bnj13

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	w-bnj13 35377	. 2 wff 𝑅 Se 𝐴
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1568	. . . . 5 class 𝑥
6	1, 2, 5	c-bnj14 35375	. . . 4 class pred(𝑥, 𝐴, 𝑅)
7		cvv 3454	. . . 4 class V
8	6, 7	wcel 2146	. . 3 wff pred(𝑥, 𝐴, 𝑅) ∈ V
9	8, 4, 1	wral 3080	. 2 wff ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V
10	3, 9	wb 209	1 wff (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 pred(𝑥, 𝐴, 𝑅) ∈ V)

This definition is used by:  bnj93  35549  bnj1489  35742