Metamath Proof Explorer


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 φ A B
Assertion xpcoidgend φ A × B A × B = A × B

Proof

Step Hyp Ref Expression
1 xpcoidgend.1 φ A B
2 incom A B = B A
3 2 1 eqnetrrid φ B A
4 3 xpcogend φ A × B A × B = A × B