Definition df-se

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

	Ref	Expression
Assertion	df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wse	$$wffR\mathrm{Se}A$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	3	cv	$$setvarx$$
7	5 6 0	wbr	$$wffyRx$$
8	7 4 1	crab	$$class\left\{y\in A|yRx\right\}$$
9		cvv	$$class\mathrm{V}$$
10	8 9	wcel	$$wff\left\{y\in A|yRx\right\}\in \mathrm{V}$$
11	10 3 1	wral	$$wff\forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
12	2 11	wb	$$wff\left(R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}\right)$$