Theorem exse2

Description: Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	exse2	$$⊢R\in V\to R\mathrm{Se}A$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{y\in A|yRx\right\}=\left\{y|\left(y\in A\wedge yRx\right)\right\}$$
2		vex	$$⊢y\in \mathrm{V}$$
3		vex	$$⊢x\in \mathrm{V}$$
4	2 3	breldm	$$⊢yRx\to y\in \mathrm{dom}R$$
5	4	adantl	$$⊢\left(y\in A\wedge yRx\right)\to y\in \mathrm{dom}R$$
6	5	abssi	$$⊢\left\{y|\left(y\in A\wedge yRx\right)\right\}\subseteq \mathrm{dom}R$$
7	1 6	eqsstri	$$⊢\left\{y\in A|yRx\right\}\subseteq \mathrm{dom}R$$
8		dmexg	$$⊢R\in V\to \mathrm{dom}R\in \mathrm{V}$$
9		ssexg	$$⊢\left(\left\{y\in A|yRx\right\}\subseteq \mathrm{dom}R\wedge \mathrm{dom}R\in \mathrm{V}\right)\to \left\{y\in A|yRx\right\}\in \mathrm{V}$$
10	7 8 9	sylancr	$$⊢R\in V\to \left\{y\in A|yRx\right\}\in \mathrm{V}$$
11	10	ralrimivw	$$⊢R\in V\to \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
12		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
13	11 12	sylibr	$$⊢R\in V\to R\mathrm{Se}A$$