Theorem idinxpss

Description: Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019)

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

Proof

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