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 )