Metamath Proof Explorer


Theorem txprel

Description: A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion txprel Rel A B

Proof

Step Hyp Ref Expression
1 txpss3v A B V × V × V
2 xpss V × V × V V × V
3 1 2 sstri A B V × V
4 df-rel Rel A B A B V × V
5 3 4 mpbir Rel A B