Theorem seinxp

Description: Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	seinxp	$$⊢R\mathrm{Se}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Se}A$$

Proof

Step	Hyp	Ref	Expression
1		brinxp	$$⊢\left(y\in A\wedge x\in A\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)$$
2	1	ancoms	$$⊢\left(x\in A\wedge y\in A\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)$$
3	2	rabbidva	$$⊢x\in A\to \left\{y\in A|yRx\right\}=\left\{y\in A|y\left(R\cap \left(A\times A\right)\right)x\right\}$$
4	3	eleq1d	$$⊢x\in A\to \left(\left\{y\in A|yRx\right\}\in \mathrm{V}\leftrightarrow \left\{y\in A|y\left(R\cap \left(A\times A\right)\right)x\right\}\in \mathrm{V}\right)$$
5	4	ralbiia	$$⊢\forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}\leftrightarrow \forall x\in A\left\{y\in A|y\left(R\cap \left(A\times A\right)\right)x\right\}\in \mathrm{V}$$
6		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|yRx\right\}\in \mathrm{V}$$
7		df-se	$$⊢\left(R\cap \left(A\times A\right)\right)\mathrm{Se}A\leftrightarrow \forall x\in A\left\{y\in A|y\left(R\cap \left(A\times A\right)\right)x\right\}\in \mathrm{V}$$
8	5 6 7	3bitr4i	$$⊢R\mathrm{Se}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Se}A$$