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 
|- Rel ( A X. B )

Proof

Step Hyp Ref Expression
1 xpss 
 |-  ( A X. B ) C_ ( _V X. _V )
2 df-rel 
 |-  ( Rel ( A X. B ) <-> ( A X. B ) C_ ( _V X. _V ) )
3 1 2 mpbir 
 |-  Rel ( A X. B )