Theorem inxp2

Description: Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019)

	Ref	Expression
Assertion	inxp2	$$⊢R\cap \left(A\times B\right)=\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge xRy\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		relinxp	$$⊢\mathrm{Rel}\left(R\cap \left(A\times B\right)\right)$$
2		dfrel4v	$$⊢\mathrm{Rel}\left(R\cap \left(A\times B\right)\right)\leftrightarrow R\cap \left(A\times B\right)=\left\{⟨x,y⟩|x\left(R\cap \left(A\times B\right)\right)y\right\}$$
3	1 2	mpbi	$$⊢R\cap \left(A\times B\right)=\left\{⟨x,y⟩|x\left(R\cap \left(A\times B\right)\right)y\right\}$$
4		brinxp2	$$⊢x\left(R\cap \left(A\times B\right)\right)y\leftrightarrow \left(\left(x\in A\wedge y\in B\right)\wedge xRy\right)$$
5	4	opabbii	$$⊢\left\{⟨x,y⟩|x\left(R\cap \left(A\times B\right)\right)y\right\}=\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge xRy\right)\right\}$$
6	3 5	eqtri	$$⊢R\cap \left(A\times B\right)=\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge xRy\right)\right\}$$