Metamath Proof Explorer


Theorem relxp

Description: A Cartesian product is a relation. Theorem 3.13(i) of Monk1 p. 37. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion relxp RelA×B

Proof

Step Hyp Ref Expression
1 xpss A×BV×V
2 df-rel RelA×BA×BV×V
3 1 2 mpbir RelA×B