Theorem exse2

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

	Ref	Expression
Assertion	exse2	|- ( R e. V -> R Se A )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { y e. A | y R x } = { y | ( y e. A /\ y R x ) }
2		vex	|- y e. _V
3		vex	|- x e. _V
4	2 3	breldm	|- ( y R x -> y e. dom R )
5	4	adantl	|- ( ( y e. A /\ y R x ) -> y e. dom R )
6	5	abssi	|- { y | ( y e. A /\ y R x ) } C_ dom R
7	1 6	eqsstri	|- { y e. A | y R x } C_ dom R
8		dmexg	|- ( R e. V -> dom R e. _V )
9		ssexg	|- ( ( { y e. A | y R x } C_ dom R /\ dom R e. _V ) -> { y e. A | y R x } e. _V )
10	7 8 9	sylancr	|- ( R e. V -> { y e. A | y R x } e. _V )
11	10	ralrimivw	|- ( R e. V -> A. x e. A { y e. A | y R x } e. _V )
12		df-se	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
13	11 12	sylibr	|- ( R e. V -> R Se A )