This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )