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

Metamath Proof Explorer

Theorem dfse2

Description: Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dfse2 
|- ( R Se A <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )

Proof

Step Hyp Ref Expression
1 df-se 
 |-  ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
2 dfrab3 
 |-  { y e. A | y R x } = ( A i^i { y | y R x } )
3 iniseg 
 |-  ( x e. _V -> ( `' R " { x } ) = { y | y R x } )
4 3 elv 
 |-  ( `' R " { x } ) = { y | y R x }
5 4 ineq2i 
 |-  ( A i^i ( `' R " { x } ) ) = ( A i^i { y | y R x } )
6 2 5 eqtr4i 
 |-  { y e. A | y R x } = ( A i^i ( `' R " { x } ) )
7 6 eleq1i 
 |-  ( { y e. A | y R x } e. _V <-> ( A i^i ( `' R " { x } ) ) e. _V )
8 7 ralbii 
 |-  ( A. x e. A { y e. A | y R x } e. _V <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )
9 1 8 bitri 
 |-  ( R Se A <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )