Theorem exse

Description: Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	exse	$$⊢A\in V\to R\mathrm{Se}A$$

Proof

Step	Hyp	Ref	Expression
1		rabexg	$$⊢A\in V\to \left\{y\in A|yRx\right\}\in \mathrm{V}$$
2	1	ralrimivw	$$⊢A\in V\to \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
3		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
4	2 3	sylibr	$$⊢A\in V\to R\mathrm{Se}A$$