Theorem inxpssidinxp

Description: Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 . (Contributed by Peter Mazsa, 4-Jul-2019)

	Ref	Expression
Assertion	inxpssidinxp	$$⊢R\cap \left(A\times B\right)\subseteq \mathrm{I}\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		inxpss2	$$⊢R\cap \left(A\times B\right)\subseteq \mathrm{I}\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to x\mathrm{I}y\right)$$
2		ideqg	$$⊢y\in \mathrm{V}\to \left(x\mathrm{I}y\leftrightarrow x=y\right)$$
3	2	elv	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
4	3	imbi2i	$$⊢\left(xRy\to x\mathrm{I}y\right)\leftrightarrow \left(xRy\to x=y\right)$$
5	4	2ralbii	$$⊢\forall x\in A\forall y\in B\left(xRy\to x\mathrm{I}y\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to x=y\right)$$
6	1 5	bitri	$$⊢R\cap \left(A\times B\right)\subseteq \mathrm{I}\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(xRy\to x=y\right)$$