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	$$⊢\left(R\mathrm{Se}A\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall y\in A\left\{x\in A|xRy\right\}\in \mathrm{V}$$
2		breq2	$$⊢y=B\to \left(xRy\leftrightarrow xRB\right)$$
3	2	rabbidv	$$⊢y=B\to \left\{x\in A|xRy\right\}=\left\{x\in A|xRB\right\}$$
4	3	eleq1d	$$⊢y=B\to \left(\left\{x\in A|xRy\right\}\in \mathrm{V}\leftrightarrow \left\{x\in A|xRB\right\}\in \mathrm{V}\right)$$
5	4	rspccva	$$⊢\left(\forall y\in A\left\{x\in A|xRy\right\}\in \mathrm{V}\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$
6	1 5	sylanb	$$⊢\left(R\mathrm{Se}A\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$