Definition df-se

Description: Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014)

	Ref	Expression
Assertion	df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	wse	⊢ 𝑅 Se 𝐴
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5	4	cv	⊢ 𝑦
6	3	cv	⊢ 𝑥
7	5 6 0	wbr	⊢ 𝑦 𝑅 𝑥
8	7 4 1	crab	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 }
9		cvv	⊢ V
10	8 9	wcel	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V
11	10 3 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V
12	2 11	wb	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )