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 e. V -> R Se A )

Proof

Step	Hyp	Ref	Expression
1		rabexg	|- ( A e. V -> { y e. A | y R x } e. _V )
2	1	ralrimivw	|- ( A e. V -> A. x e. A { y e. A | y R x } e. _V )
3		df-se	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
4	2 3	sylibr	|- ( A e. V -> R Se A )