Theorem idinxpssinxp4

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 ). (Contributed by Peter Mazsa, 8-Mar-2019)

	Ref	Expression
Assertion	idinxpssinxp4	$$⊢\forall x\in A\forall y\in A\left(x=y\to xRy\right)\leftrightarrow \forall x\in AxRx$$

Proof

Step	Hyp	Ref	Expression
1		idinxpssinxp	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in A\forall y\in A\left(x=y\to xRy\right)$$
2		idinxpssinxp2	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq R\cap \left(A\times A\right)\leftrightarrow \forall x\in AxRx$$
3	1 2	bitr3i	$$⊢\forall x\in A\forall y\in A\left(x=y\to xRy\right)\leftrightarrow \forall x\in AxRx$$