Theorem idinxpssinxp2

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	idinxpssinxp2	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in AxRx$$

Proof

Step	Hyp	Ref	Expression
1		idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$
2	1	sseq1i	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow {\mathrm{I}\upharpoonright }_A\subseteq R\cap \left(A\times A\right)$$
3		idrefALT	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in Ax\left(R\cap \left(A\times A\right)\right)x$$
4		brinxp2	$$⊢x\left(R\cap \left(A\times A\right)\right)x\leftrightarrow \left(\left(x\in A\wedge x\in A\right)\wedge xRx\right)$$
5		pm4.24	$$⊢x\in A\leftrightarrow \left(x\in A\wedge x\in A\right)$$
6	5	anbi1i	$$⊢\left(x\in A\wedge xRx\right)\leftrightarrow \left(\left(x\in A\wedge x\in A\right)\wedge xRx\right)$$
7	4 6	bitr4i	$$⊢x\left(R\cap \left(A\times A\right)\right)x\leftrightarrow \left(x\in A\wedge xRx\right)$$
8	7	ralbii	$$⊢\forall x\in Ax\left(R\cap \left(A\times A\right)\right)x\leftrightarrow \forall x\in A\left(x\in A\wedge xRx\right)$$
9	2 3 8	3bitri	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in A\left(x\in A\wedge xRx\right)$$
10		ralanid	$$⊢\forall x\in A\left(x\in A\wedge xRx\right)\leftrightarrow \forall x\in AxRx$$
11	9 10	bitri	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in AxRx$$