Theorem seex

Description: The R -preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014)

	Ref	Expression
Assertion	seex	|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-se	|- ( R Se A <-> A. y e. A { x e. A | x R y } e. _V )
2		breq2	|- ( y = B -> ( x R y <-> x R B ) )
3	2	rabbidv	|- ( y = B -> { x e. A | x R y } = { x e. A | x R B } )
4	3	eleq1d	|- ( y = B -> ( { x e. A | x R y } e. _V <-> { x e. A | x R B } e. _V ) )
5	4	rspccva	|- ( ( A. y e. A { x e. A | x R y } e. _V /\ B e. A ) -> { x e. A | x R B } e. _V )
6	1 5	sylanb	|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )