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 ) |
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 ) |