Theorem idinxpssinxp

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

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

Proof

Step	Hyp	Ref	Expression
1		inxpss2	$$⊢\mathrm{I}\cap \left(A\times B\right)\subseteq R\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(x\mathrm{I}y\to xRy\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	imbi1i	$$⊢\left(x\mathrm{I}y\to xRy\right)\leftrightarrow \left(x=y\to xRy\right)$$
5	4	2ralbii	$$⊢\forall x\in A\forall y\in B\left(x\mathrm{I}y\to xRy\right)\leftrightarrow \forall x\in A\forall y\in B\left(x=y\to xRy\right)$$
6	1 5	bitri	$$⊢\mathrm{I}\cap \left(A\times B\right)\subseteq R\cap \left(A\times B\right)\leftrightarrow \forall x\in A\forall y\in B\left(x=y\to xRy\right)$$