Definition df-bnj13

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	w-bnj13	⊢ 𝑅 Se 𝐴
3		vx	⊢ 𝑥
4	3	cv	⊢ 𝑥
5	1 0 4	c-bnj14	⊢ pred ( 𝑥 , 𝐴 , 𝑅 )
6		cvv	⊢ V
7	5 6	wcel	⊢ pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V
8	7 3 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V
9	2 8	wb	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )