Theorem inxpss2

Description: Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019)

	Ref	Expression
Assertion	inxpss2	$$⊢R\cap \left(A\times B\right)\subseteq S\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to xSy\right)$$

Proof

Step	Hyp	Ref	Expression
1		relinxp	$$⊢\mathrm{Rel}\left(R\cap \left(A\times B\right)\right)$$
2		ssrel3	$$⊢\mathrm{Rel}\left(R\cap \left(A\times B\right)\right)\to \left(R\cap \left(A\times B\right)\subseteq S\cap \left(A\times B\right)\leftrightarrow \forall x\forall y\left(x\left(R\cap \left(A\times B\right)\right)y\to x\left(S\cap \left(A\times B\right)\right)y\right)\right)$$
3	1 2	ax-mp	$$⊢R\cap \left(A\times B\right)\subseteq S\cap \left(A\times B\right)\leftrightarrow \forall x\forall y\left(x\left(R\cap \left(A\times B\right)\right)y\to x\left(S\cap \left(A\times B\right)\right)y\right)$$
4		inxpss3	$$⊢\forall x\forall y\left(x\left(R\cap \left(A\times B\right)\right)y\to x\left(S\cap \left(A\times B\right)\right)y\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to xSy\right)$$
5	3 4	bitri	$$⊢R\cap \left(A\times B\right)\subseteq S\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to xSy\right)$$