Metamath Proof Explorer


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 )