Theorem xpcoidgend

Description: If two classes are not disjoint, then the composition of their Cartesian product with itself is idempotent. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypothesis	xpcoidgend.1	$$⊢\phi \to A\cap B\ne \varnothing$$
Assertion	xpcoidgend	$$⊢\phi \to \left(A\times B\right)\circ \left(A\times B\right)=A\times B$$

Proof

Step	Hyp	Ref	Expression
1		xpcoidgend.1	$$⊢\phi \to A\cap B\ne \varnothing$$
2		incom	$$⊢A\cap B=B\cap A$$
3	2 1	eqnetrrid	$$⊢\phi \to B\cap A\ne \varnothing$$
4	3	xpcogend	$$⊢\phi \to \left(A\times B\right)\circ \left(A\times B\right)=A\times B$$