Theorem txprel

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

	Ref	Expression
Assertion	txprel	|- Rel ( A (x) B )

Proof

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